[Ada] Adapt proof of double arithmetic runtime unit

[Ada] Adapt proof of double arithmetic runtime unit

After changes in Why3 and generation of VCs, ghost code needs to be
adapted for proofs to remain automatic.

gcc/ada/

	* libgnat/s-aridou.adb (Big3): Change return type.
	(Lemma_Mult_Non_Negative, Lemma_Mult_Non_Positive): Reorder
	alphabetically.
	(Lemma_Concat_Definition, Lemma_Double_Big_2xxsingle): New
	lemmas.
	(Double_Divide, Scaled_Divide): Add assertions.