This proves the generic unit System.Exponu instantiated for Unsigned,
Long_Long_Unsigned and Long_Long_Long_Unsigned. The proof is simpler
than the one for signed integers, as there are no possible overflows
here.

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

gcc/ada/

	* libgnat/s-explllu.ads: Mark in SPARK.
	* libgnat/s-expllu.ads: Mark in SPARK.
	* libgnat/s-exponu.adb: Add loop invariants and needed
	assertions.
	* libgnat/s-exponu.ads: Add functional contract.
	* libgnat/s-expuns.ads: Mark in SPARK.