ada: Update proof of runtime units

ada: Update proof of runtime units

Following changes in GNATprove, proofs need to be amended.

gcc/ada/

	* libgnat/s-aridou.adb (Lemma_Div_Pow2): Add assertion.
	* libgnat/s-arit32.adb (Lemma_Abs_Div_Commutation): Simplify.
	* libgnat/s-expmod.adb (Lemma_Exp_Mod): Add assertions.
	(Lemma_Euclidean_Mod): Add body to lemma.
	(Lemma_Mult_Mod): Add assertion.
	* libgnat/s-valueu.adb (Scan_Raw_Unsigned): Modify assertion.
	* libgnat/s-vauspe.ads (Raw_Unsigned_Last_Ghost): Add
	postcondition.
	* libgnat/s-widthi.adb: Use more precise types.