This replicates the proofs performed for 'Width on modular integers to
the units that support 'Width on signed integers. Also add a minimal
postcondition to the System.Width_U.

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

gcc/ada/

	* libgnat/s-widint.ads: Mark in SPARK.
	* libgnat/s-widlli.ads: Likewise.
	* libgnat/s-widllli.ads: Likewise.
	* libgnat/s-widlllu.ads: Likewise.
	* libgnat/s-widllu.ads: Disable ghost/contract.
	* libgnat/s-widthi.adb: Replicate and adapt the proof from
	s-widthu.adb.
	* libgnat/s-widthi.ads: Add minimal postcondition.
	* libgnat/s-widthu.adb: Fix comments in the modular case.
	* libgnat/s-widthu.ads: Add minimal postcondition.
	* libgnat/s-widuns.ads: Disable ghost/contract.