recfun div_alt(a:Nat, b:Nat, y:Nat) -> Pair<Nat,Nat>
measure	(a + b) + b  {
  if b = zero then
    pair(zero, a)
  else
    if (a = y and zero < a) then
      define f = div_alt(zero, b, y);
	pair(suc(first(f)), second(f))
    else
      div_alt(suc(a), b ∸ suc(zero), y)
}

fun divides(a:Nat, b:Nat) {
  some k:Nat. a * k = b
}

fun operator %(n:Nat, m:Nat) {
  n ∸ (n / m) * m
}

recfun operator /(n:Nat, m:Nat) -> Nat
measure	n  {
  if n < m then
    zero
  else
    if m = zero then
      zero
    else
      suc(zero) + (n ∸ m) / m
}

strong_induction: (all P:(fn Nat -> bool), n:Nat. (if (all j:Nat. (if (all i:Nat. (if i < j then P(i))) then P(j))) then P(n)))