ada: Adapt proofs of light runtime to current version of SPARK

ada: Adapt proofs of light runtime to current version of SPARK

gcc/ada/ChangeLog:

	* libgnat/a-strmap.adb: Add assert to regain proofs.
	* libgnat/a-strsup.adb: Likewise.
	* libgnat/s-aridou.adb: Add assertions to regain proofs.
	* libgnat/s-arit32.adb: Use Exceptional_Cases to specify Raise.
	* libgnat/s-arit64.adb: Use Round_Quatient from Impl instead of
	redefining it.
	* libgnat/s-arit64.ads: Likewise.
	* libgnat/s-expmod.adb: Regain proof of lemma.
	* libgnat/s-exponn.adb: Likewise.
	* libgnat/s-expont.adb: Likewise.
	* libgnat/s-imgboo.adb: Add local lemma to regain proof.
	* libgnat/s-valuti.ads: Add Always_Terminates on Bad_Value.