from remainder := n
	 invariant reversible: n = Result*divisor+remainder
	 variant decreasing_remainder: remainder
	 until remainder < divisor
	 loop
	    remainder := remainder - divisor
	    Result := Result + 1
	 end --loop