recfun div_alt(a:Nat, b:Nat, y:Nat) -> Pair<Nat,Nat>
  measure (a + b) + b of Nat
{
  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)
}
terminates {
  arbitrary a.s40_4 : Nat,
  b.s40_5 : Nat,
  y.s40_6 : Nat
  have A: (if (b ≠ zero and (a = y) and (zero < a)) then (zero + b) + b < (a + b) + b) by {
    assume prem.s40_7
    have X: b + b < (b + b) + a by {
      apply less_add_pos[b + b, a] to prem
    }
    replace add_commute[a, b + b]
X
  }
  have B: (if (b ≠ zero and not ((a = y) and (zero < a))) then (suc(a) + (b ∸ suc(zero))) + (b ∸ suc(zero)) < (a + b) + b) by {
    assume prem.s40_10
    obtain b'.s40_11 where bs.s40_12 : b = suc(b') from apply not_zero_suc[b] to prem
    replace bs
    expand operator ∸
    replace monus_zero | add_suc | add_suc
    expand operator + | operator + | operator < | operator ≤ | operator ≤
less_equal_refl
  }
A, B
}

define divides : (fn (Nat, Nat) -> bool) = fun a:Nat, b:Nat {
      some k:Nat. a * k = b
    }

define operator % : (fn (Nat, Nat) -> Nat) = fun n:Nat, m:Nat {
      n ∸ (n / m) * m
    }

recfun operator /(n:Nat, m:Nat) -> Nat
  measure n of Nat
{
  if n < m then
    zero
  else
    if m = zero then
      zero
    else
      suc(zero) + (n ∸ m) / m
}
terminates {
  arbitrary n.s21_3 : Nat,
  m.s21_4 : Nat
  assume cond.s21_5: (not (n < m) and m ≠ zero)
  suffices m + (n ∸ m) < m + n  by {
add_both_sides_of_less[m, n ∸ m, n]
  }
  suffices n < m + n  by {
    have m_n: m ≤ n by {
      apply not_less_implies_less_equal to conjunct 0 of cond
    }
    replace (apply monus_add_identity[n, m] to m_n)
.
  }
  obtain m'.s21_7 where m_sm.s21_8 : m = suc(m') from apply not_zero_suc to conjunct 1 of cond
  suffices n < suc(m') + n  by {
    replace m_sm
.
  }
  suffices n ≤ m' + n  by {
    expand operator + | operator < | operator ≤
.
  }
  replace add_commute
  conclude n ≤ n + m' by {
less_equal_add
  }
}

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)))