[Ada] Fix proof of runtime unit System.Wid_*

Regain the proof of System.Wid_* after changes in provers and Why3.

gcc/ada/

	* libgnat/s-widthu.adb (Lemma_Euclidean): Lemma to prove the
	relation between the quotient/remainder of a division.