ada: Restore proof of System.Arith_Double

ada: Restore proof of System.Arith_Double

Use Assert_And_Cut to simplify proof of second part of the Scaled_Divide.
Add intermediate assertions and simplify where necessary.

gcc/ada/

	* libgnat/s-aridou.adb:
	(Big3): Remove override made useless.
	(Lemma_Quot_Rem): Add new lemma and justify it, as no prover
	manages to prove it.
	(Lemma_Div_Pow2): Use new lemma Lemma_Quot_Rem.
	(Prove_Scaled_Mult_Decomposition_Regroup3): Retype for
	simplification.
	(Scaled_Divide): Remove useless assertions.Decompose some
	assertions with cut operations. Use Assert_And_Cut for second
	half. Add assertions.