[Ada] Amend proof of System.Arith_Double to remove justifications

[Ada] Amend proof of System.Arith_Double to remove justifications

gcc/ada/

	* libgnat/s-aridou.adb (Log_Single_Size, Big_0): New ghost
	constants.
	(Lemma_Mult_Non_Negative, Lemma_Mult_Non_Positive,
	Lemma_Not_In_Range_Big2xx64): New lemmas on big integers.
	(Double_Divide): Remove justifications. Amend for that local
	lemma Prove_Overflow_Case.
	(Scaled_Divide): Remove justifications. Insert for that local
	lemmas Prove_Negative_Dividend, Prove_Positive_Dividend and
	Prove_Q_Too_Big, and amend local lemma Prove_Overflow.  To prove
	the loop invariant on (Shift mod 2 = 0), introduce local ghost
	variable Iter to count loop iterations, and relate its value to
	the value of Shift through Log_Single_Size, with the help of
	local lemma Prove_Power. Deal with proof regression by adding
	new local lemma Prove_First_Iteration and local ghost variable
	D123.
	* libgnat/s-arit64.ads (Multiply_With_Ovflo_Check64): Remove
	unnecessary Pure_Function on function as package is Pure.