[Ada] Further adapt proof of double arithmetic runtime unit

[Ada] Further 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 (Lemma_Abs_Range,
	Lemma_Double_Shift_Left, Lemma_Shift_Left): New lemmas.
	(Double_Divide): Add ghost code.
	(Lemma_Concat_Definition, Lemma_Double_Shift_Left,
	Lemma_Shift_Left, Lemma_Shift_Right): Define or complete lemmas.
	(Scaled_Divide): Add ghost code.