[Ada] Recover proof of Scaled_Divide in System.Arith_64

Proof of Scaled_Divide was impacted by changes in provers and Why3.
Recover it partially, leaving some unproved basic inferences to be
further investigated.

gcc/ada/

	* libgnat/s-aridou.adb: Add or rework ghost code.
	* libgnat/s-aridou.ads: Add Big_Positive subtype.