After changes in provers and Why3, changes are needed to recover
automatic proof of System.Arith_64. This is the first part of it.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* libgnat/s-aridou.adb (Lemma_Mult_Div, Lemma_Powers): New
	lemmas.
	(Prove_Sign_Quotient): New local lemma.
	(Prove_Signs): Expand definition of Big_R and Big_Q in the
	postcondition. Add intermediate assertions.
	(Double_Divide): Call new lemma.
	(Lemma_Div_Eq): Provide body for proving lemma.
	(Lemma_Powers_Of_2, Lemma_Shift_Without_Drop,
	Prove_Dividend_Scaling, Prove_Multiplication, Prove_Z_Low): Call
	lemmas, add intermediate assertions.