module Nat

import Option
import Base

/*
  Public entry point for natural numbers.

  This module re-exports the Nat definition, arithmetic, order,
  division, parity, powers/logarithms, and summation support, then
  adds cross-cutting facts such as boolean equality, gcd, and literal
  arithmetic rewrite support.
*/

public import NatDefs
public import NatAdd
public import NatMonus
public import NatMult
public import NatLess
public import NatDiv
public import NatEvenOdd
public import NatPowLog
public import NatSum

/*
 Properties of equal
*/

// The boolean-valued `equal` is reflexive.
theorem equal_refl: all n:Nat. equal(n,n)
proof
  induction Nat
  case zero {
    expand equal.
  }
  case suc(n') suppose IH {
    suffices equal(n',n')  by expand equal.
    IH
  }
end

// Propositional equality on Nat is equivalent to its boolean `equal`.
theorem equal_complete_sound : all m:Nat. all n:Nat.
  m = n ⇔ equal(m, n)
proof
  induction Nat
  case zero {
    arbitrary n:Nat
    switch n {
      case zero { expand equal. }
      case suc(n') { expand equal. }
    }
  }
  case suc(m') suppose IH {
    arbitrary n:Nat 
    switch n {
      case zero { expand equal. }
      case suc(n') {
        have right : (if suc(m') = suc(n') then equal(suc(m'), suc(n')))
          by suppose sm_sn: suc(m') = suc(n')
             suffices equal(m', n')  by expand equal.
             have m_n: m' = n' by injective suc sm_sn
             suffices equal(n', n')  by replace m_n.
             equal_refl[n']
        have left : (if equal(suc(m'), suc(n')) then suc(m') = suc(n'))
          by suppose sm_sn : equal(suc(m'), suc(n'))
             have e_m_n : equal(m', n') by expand equal in sm_sn
             have m_n : m' = n' by apply IH to e_m_n
             replace m_n.
        right, left
      }
    }
  }
end

// Boolean inequality implies propositional inequality.
theorem not_equal_not_eq: all m:Nat, n:Nat.
  if not equal(m, n) then not (m = n)
proof
  arbitrary m:Nat, n:Nat
  suppose not_m_n
  suppose m_n
  have eq_m_n: equal(m, n) by {
    suffices equal(n,n)  by replace m_n.
    equal_refl[n]
  }
  apply not_m_n to eq_m_n
end

/*
  Greatest Common Divisor
*/

// Euclidean gcd: recurses on `a % b` until the second argument is zero,
// at which point the first argument is the gcd.
recfun gcd(a : Nat, b : Nat) -> Nat
  measure b of Nat
{
  if b = zero then a
  else gcd(b, a % b)
}
terminates {
  arbitrary a:Nat, b:Nat
  assume bnz: not (b = zero)
  have b_pos: zero < b  by apply or_not to zero_or_positive[b], bnz
  conclude a % b < b by apply mod_less_divisor[a,b] to b_pos
}

// `gcd(a,b)` is a common divisor of `a` and `b`.
theorem gcd_divides: all b:Nat, a:Nat. divides(gcd(a,b), a) and divides(gcd(a,b), b)
proof
  define P = fun b':Nat {all a:Nat. divides(gcd(a,b'), a) and divides(gcd(a,b'), b')}
  have X: all j:Nat. (if (all i:Nat. (if i < j then P(i))) then P(j)) by {
    arbitrary j:Nat
    assume IH: all i:Nat. (if i < j then P(i))
    expand P
    switch j {
      case zero {
        arbitrary a:Nat
        have A: divides(gcd(a, zero), a) by {
          expand divides | gcd
          choose suc(zero)
          conclude a * suc(zero) = a  by mult_one
        }
        have B: divides(gcd(a, zero), zero) by {
          expand divides | gcd
          choose zero
          conclude a * zero = zero  by mult_zero
        }
        A, B
      }
      case suc(j') assume j_suc {
        arbitrary a:Nat
        replace symmetric j_suc
        have j_pos: zero < j by {
          replace recall j = suc(j')
          evaluate
        }
        have smaller: a % j < j
          by apply mod_less_divisor[a,j] to j_pos
        have div_j_div_aj: divides(gcd(j, a % j), j) and divides(gcd(j, a % j), a % j)
          by (expand P in apply IH[a%j] to smaller)[j]
        have A: divides(gcd(a, j), a) by {
          replace j_suc expand gcd replace symmetric j_suc
          conclude divides(gcd(j, a % j), a)
            by apply divides_mod[gcd(j, a % j), a, j] to div_j_div_aj, j_pos
        }
        have B: divides(gcd(a, j), j) by {
          replace j_suc expand gcd replace symmetric j_suc
          conclude divides(gcd(j, a % j), j) by div_j_div_aj
        }
        A, B
      }
    }
  }
  arbitrary b:Nat
  expand P in apply strong_induction[P,b] to X
end

/*
  Support for automatic arithmetic on literals.
*/

// Truncated subtraction from literal zero is zero.
theorem nat_zero_monus: all m:Nat.
  lit(zero) ∸ lit(m) = lit(zero)
proof
  arbitrary m:Nat
  expand lit | operator∸.
end

// Subtracting literal zero leaves the operand unchanged.
theorem nat_monus_zero: all n:Nat.
  n ∸ lit(zero) = n
proof
  arbitrary n:Nat
  expand lit
  monus_zero
end

auto nat_monus_zero

// Successor cancels on both sides of truncated subtraction.
theorem lit_suc_monus_suc: all n:Nat, m:Nat.
  lit(suc(n)) ∸ lit(suc(m)) = lit(n) ∸ lit(m)
proof
  arbitrary n:Nat, m:Nat
  expand lit | operator∸.
end

auto lit_suc_monus_suc

// Multiplication by a literal distributes over a sum on the right.
theorem lit_dist_mult_add:
  all a:Nat, x:Nat, y:Nat.
  lit(a) * (x + y) = lit(a) * x + lit(a) * y
proof
  arbitrary a:Nat, x:Nat, y:Nat
  expand lit
  dist_mult_add
end

auto lit_dist_mult_add

// Multiplication by a literal distributes over a sum on the left.
theorem lit_dist_mult_add_right:
  all x:Nat, y:Nat, a:Nat.
  (x + y) * lit(a) = x * lit(a) + y * lit(a)
proof
  arbitrary x:Nat, y:Nat, a:Nat
  expand lit
  dist_mult_add_right
end

auto lit_dist_mult_add_right

// Doubling expressed as multiplication by literal two.
theorem mult_two: all n:Nat.
  n + n = lit(suc(suc(zero))) * n
proof
  arbitrary n:Nat
  expand lit
  replace two_mult.
end

// Pull `suc` out of a literal-prefixed sum into the literal.
theorem lit_suc_add2: all x:Nat, y:Nat.
  suc(lit(x) + y) = lit(suc(x)) + y
proof
  arbitrary x:Nat, y:Nat
  expand lit
  replace suc_add.
end

// This causes problem with pattern matching in switch. -Jeremy
//auto lit_suc_add2

// The following causes infinite loop for
// lit(x) * lit(y)

// theorem lit_mult_commute: all n:Nat, m:Nat.
//   n * lit(m) = lit(m) * n
// proof
//   arbitrary n:Nat, m:Nat
//   expand lit
//   mult_commute
// end

// auto lit_mult_commute

// Shift a `suc` from the right operand into the literal on the left.
theorem lit_add_suc: all n:Nat, m:Nat.
  lit(n) + suc(m) = lit(suc(n)) + m
proof
  arbitrary n:Nat, m:Nat
  expand lit
  replace add_suc
  expand operator+.
end

auto lit_add_suc

// Left cancellation of multiplication when the literal factor is positive.
theorem lit_mult_left_cancel : all m : Nat, a : Nat, b : Nat.
  if lit(suc(m)) * a = lit(suc(m)) * b then a = b
proof
  arbitrary m : Nat, a : Nat, b : Nat
  expand lit
  mult_left_cancel
end

/*
  More Properties of Summation
  */

// Closed form: twice the sum 0+1+...+(n-1) equals n*(n-1).
theorem sum_n : all n : Nat.
    ℕ2 * summation(n, ℕ0, λ x {x}) = n * (n ∸ ℕ1)
proof
    induction Nat
    case zero {
        evaluate
    }
    case suc(n') suppose IH {
      have step1: (all i:Nat. (if i < ℕ1 then n' + i = ℕ0 + (n' + i))) by {
        arbitrary i:Nat
        suppose prem : i < ℕ1
        evaluate
      }
      replace nat_suc_one_add[n']
      | add_commute[ℕ1, n']
      | apply summation_add[n', ℕ1, ℕ0, n', λn{n}, λn{n}, λn{n}] to step1
      | IH
      expand lit | 2* summation
      replace nat_suc_one_add | add_commute[n', ℕ1]
      replace add_monus_identity
      replace nat_suc_one_add | dist_mult_add_right
      replace mult_commute[n', n' ∸ ℕ1]
      replace symmetric dist_mult_add_right[n' ∸ ℕ1, ℕ2, n']
      switch n' {
        case zero {
          .
        }
        case suc(n'') {
          replace nat_suc_one_add | add_monus_identity
          replace dist_mult_add | dist_mult_add_right
          replace mult_two
          replace add_commute[n'', ℕ1] | add_commute[n'', ℕ2] | add_commute[n'' * n'', ℕ2 * n''].
        }
      }
    }
end

// Geometric sum closed form: Σ_{i
// as `1 + Σ = 2^n` to stay in Nat (no monus). Proved by induction on n,
// peeling off the final term via `summation_suc_add` and reducing
// `2^(suc n') = 2 * 2^n'` to `2^n' + 2^n'`.
theorem summation_pow2_succ: all n:Nat.
  ℕ1 + summation(n, ℕ0, λ i:Nat { ℕ2 ^ i }) = ℕ2 ^ n
proof
  induction Nat
  case zero {
    expand summation
    evaluate
  }
  case suc(n') suppose IH {
    show ℕ1 + summation(suc(n'), ℕ0, λ i:Nat { ℕ2 ^ i }) = ℕ2 ^ suc(n')
    have e_suc: suc(zero) + n' = suc(n') by expand operator+.
    have step:
      summation(suc(n'), ℕ0, λ i:Nat { ℕ2 ^ i })
      = summation(n', ℕ0, λ i:Nat { ℕ2 ^ i }) + ℕ2 ^ n'
    by {
      have h1: summation(suc(zero) + n', ℕ0, λ i:Nat { ℕ2 ^ i })
             = summation(n', ℕ0, λ i:Nat { ℕ2 ^ i }) + (λ i:Nat { ℕ2 ^ i })(ℕ0 + n')
        by summation_suc_add[n', ℕ0, λ i:Nat { ℕ2 ^ i }]
      replace e_suc in h1
    }
    replace step | IH
    show ℕ2 ^ n' + ℕ2 ^ n' = ℕ2 ^ suc(n')
    have pow_step: ℕ2 ^ suc(n') = ℕ2 * ℕ2 ^ n' by expand operator^ | expt.
    replace pow_step
    symmetric lit_two_mult[ℕ2 ^ n']
  }
end

// Generic geometric sum closed form: `1 + (a − 1) · Σ_{i
// written additively so the closed form stays in Nat (no monus on the
// RHS). The premise `1 ≤ a` lets `monus_add_identity` recover
// `(a ∸ 1) + 1 = a` inside the inductive step. The pow2 specialization
// (`a = 2`, so `a ∸ 1 = 1`) recovers `summation_pow2_succ`.
theorem summation_pow_succ: all a:Nat. if ℕ1 ≤ a then
  all n:Nat.
  ℕ1 + (a ∸ ℕ1) * summation(n, ℕ0, λ i:Nat { a ^ i }) = a ^ n
proof
  arbitrary a:Nat
  assume one_le_a: ℕ1 ≤ a
  have a_eq: ℕ1 + (a ∸ ℕ1) = a by apply monus_add_identity to one_le_a
  induction Nat
  case zero {
    expand summation
    evaluate
  }
  case suc(n') suppose IH {
    show ℕ1 + (a ∸ ℕ1) * summation(suc(n'), ℕ0, λ i:Nat { a ^ i }) = a ^ suc(n')
    have e_suc: suc(zero) + n' = suc(n') by expand operator+.
    have step:
      summation(suc(n'), ℕ0, λ i:Nat { a ^ i })
      = summation(n', ℕ0, λ i:Nat { a ^ i }) + a ^ n'
    by {
      have h1: summation(suc(zero) + n', ℕ0, λ i:Nat { a ^ i })
             = summation(n', ℕ0, λ i:Nat { a ^ i }) + (λ i:Nat { a ^ i })(ℕ0 + n')
        by summation_suc_add[n', ℕ0, λ i:Nat { a ^ i }]
      replace e_suc in h1
    }
    replace step
    show ℕ1 + (a ∸ ℕ1) * (summation(n', ℕ0, λ i:Nat { a ^ i }) + a ^ n') = a ^ suc(n')

    have pow_step: a ^ suc(n') = a * a ^ n' by expand operator^ | expt.

    // `((a ∸ 1) + 1) · a^n' = a · a^n' = a^(suc n')`.
    have a_eq': (a ∸ ℕ1) + ℕ1 = a by replace add_commute in a_eq
    have d: ((a ∸ ℕ1) + ℕ1) * a ^ n' = (a ∸ ℕ1) * a ^ n' + ℕ1 * a ^ n'
      by dist_mult_add_right[a ∸ ℕ1, ℕ1, a ^ n']
    have e: a * a ^ n' = (a ∸ ℕ1) * a ^ n' + a ^ n' by replace a_eq' in d
    have collapse: (a ∸ ℕ1) * a ^ n' + a ^ n' = a ^ suc(n')
      by transitive (symmetric e) (symmetric pow_step)

    equations
          ℕ1 + (a ∸ ℕ1) * (summation(n', ℕ0, λ i:Nat { a ^ i }) + a ^ n')
        = ℕ1 + ((a ∸ ℕ1) * summation(n', ℕ0, λ i:Nat { a ^ i })
                + (a ∸ ℕ1) * a ^ n')
            by replace dist_mult_add.
    ... = (ℕ1 + (a ∸ ℕ1) * summation(n', ℕ0, λ i:Nat { a ^ i }))
            + (a ∸ ℕ1) * a ^ n'
            by symmetric add_assoc[ℕ1, (a ∸ ℕ1) * summation(n', ℕ0, λ i:Nat { a ^ i }), (a ∸ ℕ1) * a ^ n']
    ... = a ^ n' + (a ∸ ℕ1) * a ^ n'    by replace IH.
    ... = (a ∸ ℕ1) * a ^ n' + a ^ n'    by add_commute
    ... = a ^ suc(n')                    by collapse
  }
end

// Closed form: twice the sum 0+1+...+n equals n*(n+1).
theorem sum_n' : all n : Nat.
    ℕ2 * summation(suc(n), ℕ0, λ x {x}) = n * (n + ℕ1)
proof
    induction Nat
    case zero {
      expand 2* summation.
    }
    case suc(n') suppose IH {
      have step1: (all i:Nat. (if i < ℕ1 then suc(n') + i = ℕ0 + (suc(n') + i))) by {
        arbitrary i:Nat
        suppose prem : i < ℕ1
        .
      }
      replace nat_suc_one_add
      replace (replace add_commute[n',ℕ1] in
          (apply summation_add[ℕ1 + n'][ℕ1, ℕ0, suc(n'), λn{n}, λn{n}, λn{n}]
           to replace nat_suc_one_add.))
      replace (replace nat_suc_one_add in IH)
      expand lit | 2*summation
      replace nat_suc_one_add | dist_mult_add | dist_mult_add_right
      replace dist_mult_add[n', n', ℕ1] | add_commute[ℕ1, n' + n'] | mult_two[n']
      | add_commute[ℕ2 * n', ℕ2] | add_commute[ℕ2 + ℕ2 * n', n' * n' + n'].
    }
end

/*
  Public versions of theorems involving literals
*/

// Left cancellation of multiplication when the left factor is positive.
theorem pos_mult_left_cancel : all m : Nat, a : Nat, b : Nat.
  if ℕ0 < m and m * a = m * b then a = b
proof
  arbitrary m : Nat, a : Nat, b : Nat
  assume prem
  switch m {
    case zero assume mz {
      conclude false by evaluate in replace mz in prem
    }
    case suc(m') assume ms {
      apply mult_left_cancel[m', a, b] to replace ms in prem
    }
  }
end

// Right cancellation of strict inequality when the right factor is positive.
theorem pos_mult_right_cancel_less : all c : Nat, a : Nat, b : Nat.
  if ℕ0 < c and a * c < b * c then a < b
proof
  arbitrary c : Nat, a : Nat, b : Nat
  expand lit
  assume prem
  apply (apply mult_lt_mono_r[c,a,b] to prem) to prem
end

// Left cancellation of `≤` when the left factor is positive.
theorem pos_mult_left_cancel_less_equal : all n : Nat, x : Nat, y : Nat.
  if ℕ0 < n and n * x ≤ n * y then x ≤ y
proof
  arbitrary n : Nat, x : Nat, y : Nat
  expand lit
  assume prem  
  obtain n' where ns: n = suc(n') from apply positive_suc[n] to prem
  apply mult_nonzero_mono_le[n', x, y] to (replace ns in prem)
end
  
// Multiplying both sides of a strict inequality by a positive factor preserves it.
theorem pos_mult_both_sides_of_less : all n : Nat, x : Nat, y : Nat.
  if ℕ0 < n and x < y then n * x < n * y
proof
  arbitrary n : Nat, x : Nat, y : Nat
  expand lit
  assume prem
  obtain n' where ns: n = suc(n') from apply positive_suc[n] to prem
  replace ns
  apply mono_nonzero_mult_le[n', x, y] to (replace ns in prem)
end
  
// `1 + n` is positive for every `n`.
theorem nat_zero_less_one_add: all n:Nat.
  ℕ0 < ℕ1 + n
proof
  arbitrary n:Nat
  expand lit
  zero_less_one_add
end

// If two naturals sum to zero then both are zero.
theorem nat_add_to_zero: all n:Nat, m:Nat.
  if n + m = ℕ0
  then n = ℕ0 and m = ℕ0
proof
  arbitrary n:Nat, m:Nat
  expand lit
  add_to_zero
end

// Adding a positive amount strictly increases the value.
theorem nat_less_add_pos: all x:Nat, y:Nat.
  if ℕ0 < y
  then x < x + y
proof
  arbitrary x:Nat, y:Nat
  expand lit
  less_add_pos
end

// `x ≤ y` is equivalent to truncated subtraction `x ∸ y` being zero.
theorem nat_monus_zero_iff_less_eq : all x : Nat, y : Nat.
  x ≤ y  ⇔  x ∸ y = ℕ0
proof
  arbitrary x : Nat, y : Nat
  expand lit
  monus_zero_iff_less_eq[x, y]
end

// Subtracting one is the predecessor function.
theorem nat_monus_one_pred : all x : Nat. x ∸ ℕ1 = pred(x)
proof
  arbitrary x:Nat
  expand lit
  monus_one_pred
end

// Any value minus itself (truncated) is zero.
theorem nat_monus_cancel: all n:Nat. n ∸ n = ℕ0
proof
  arbitrary n:Nat
  expand lit
  monus_cancel
end

// Every natural is either zero or strictly positive.
theorem nat_zero_or_positive: all x:Nat. x = ℕ0 or ℕ0 < x
proof
  arbitrary x:Nat
  expand lit
  zero_or_positive[x]
end

// `1 + n` is never zero.
theorem nat_not_one_add_zero: all n:Nat.
  not (ℕ1 + n = ℕ0)
proof
  arbitrary n:Nat
  expand lit
  not_one_add_zero[n]
end

// Every positive natural is `1 + n'` for some `n'`.
theorem nat_positive_suc: all n:Nat.
  if ℕ0 < n
  then some n':Nat. n = ℕ1 + n'
proof
  arbitrary n:Nat
  expand lit
  assume prem
  expand operator+
  apply positive_suc[n] to prem
end

// The only natural `≤ 0` is zero itself.
theorem nat_zero_le_zero: all x:Nat. if x ≤ ℕ0 then x = ℕ0
proof
  arbitrary x:Nat
  expand lit
  zero_le_zero
end
  
// Extending the summation range by one appends `f(s + n)`.
theorem summation_next: all n:Nat, s:Nat, f:fn Nat->Nat.
  summation(ℕ1 + n, s, f) = summation(n, s, f) + f(s + n)
proof
  arbitrary n:Nat, s:Nat, f:fn Nat->Nat
  expand lit
  summation_suc_add
end

// Nothing is strictly less than zero (boolean form).
theorem less_zero_false: all x:Nat. (x < zero) = false
proof
  arbitrary x:Nat
  apply eq_false to not_less_zero[x]
end

auto less_zero_false
  
// Zero is `≤` everything (boolean form).
theorem zero_less_equal_true: all x:Nat. (zero ≤ x) = true
proof
  arbitrary x:Nat
  expand operator≤.
end

auto zero_less_equal_true

// A successor cannot be `≤ 0`.
theorem not_suc_less_equal_zero: all x:Nat. not (suc(x) ≤ zero)
proof
  arbitrary x:Nat
  expand operator≤.
end

// Literal form: `suc(x) ≤ 0` is false.
theorem lit_suc_less_equal_zero_false: all x:Nat. (lit(suc(x)) ≤ lit(zero)) = false
proof
  arbitrary x:Nat
  expand lit
  apply eq_false to not_suc_less_equal_zero[x]
end

auto lit_suc_less_equal_zero_false
  

// Successor cancels on both sides of `≤` (literal form).
theorem le_lit_suc: all x:Nat, y:Nat. (lit(suc(x)) ≤ lit(suc(y))) = (lit(x) ≤ lit(y))
proof
  arbitrary x:Nat, y:Nat
  expand lit
  replace apply iff_equal to suc_less_equal_iff_less_equal_suc[x,y].
end
auto le_lit_suc  

// Successor cancels on both sides of `<` (literal form).
theorem less_lit_suc: all x:Nat, y:Nat. (lit(suc(x)) < lit(suc(y))) = (lit(x) < lit(y))
proof
  arbitrary x:Nat, y:Nat
  expand lit
  replace apply iff_equal to less_suc_iff_suc_less[x,y].
end
auto less_lit_suc  

// Literal zero is strictly less than every successor.
theorem less_lit_zero_suc: all y:Nat. (lit(zero) < lit(suc(y))) = true
proof
  arbitrary y:Nat
  expand lit | operator< | operator≤.
end
auto less_lit_zero_suc

// Literal zero divided by any positive literal is zero.
theorem lit_zero_div: all x:Nat. lit(zero) / lit(suc(x)) = lit(zero)
proof
  arbitrary x:Nat
  have pos: zero < suc(x) by expand operator< | operator≤.
  have zero_div_theorem: lit(zero) / lit(suc(x)) = lit(zero) by {
    expand lit
    apply zero_div[suc(x)] to pos
  }
  zero_div_theorem
end
auto lit_zero_div

// A positive literal divided by itself is one.
theorem lit_div_cancel: all y:Nat. lit(suc(y)) / lit(suc(y)) = lit(suc(zero))
proof
  arbitrary y:Nat
  have pos: zero < suc(y) by expand operator< | operator≤.
  have cancel_theorem: lit(suc(y)) / lit(suc(y)) = lit(suc(zero)) by {
    expand lit
    apply div_cancel[suc(y)] to pos
  }
  cancel_theorem
end
auto lit_div_cancel

// Helper used by the literal-division `auto` rewrites below: shifts the
// quotient computation into a tail-recursive form `add_div(a,b,y) = (a+b)/y`,
// maintaining the invariant `a ≤ y`.
fun add_div(a : Nat, b : Nat, y : Nat) { (a + b) / y } // invariant: a ≤ y

// Entry rewrite: route literal division through `add_div` with accumulator zero.
theorem lit_div: all x:Nat, y:Nat. lit(x) / lit(y) = add_div(zero, x, y)
proof
  arbitrary x:Nat, y:Nat
  expand lit | add_div.
end
auto lit_div

// When the accumulator equals the divisor, emit a `1` and reset the accumulator.
theorem lit_add_div: all b:Nat, y:Nat. add_div(suc(y), b, suc(y)) = lit(suc(zero)) + add_div(zero, b, suc(y))
proof
  arbitrary b:Nat, y:Nat
  have pos: zero < suc(y) by expand operator< | operator≤.
  expand lit | add_div | operator+
  replace add_commute[y,b]
  have X: (b + suc(y)) / suc(y) = suc(zero) + b / suc(y) by apply add_div_one[b, suc(y)] to pos
  expand operator+ in replace add_suc in X
end
auto lit_add_div

// Step rewrite: move a `suc` from the dividend remainder into the accumulator.
theorem lit_add_div_suc: all a:Nat, b:Nat, y:Nat. add_div(a, suc(b), y) = add_div(suc(a), b, y)
proof
  arbitrary a:Nat, b:Nat, y:Nat
  expand add_div
  replace add_suc
  expand operator+.
end
auto lit_add_div_suc

// Terminating case: with no remaining dividend and accumulator below the divisor, the quotient is zero.
theorem lit_add_div_zero: all a:Nat, y:Nat. if a < y then add_div(a, zero, y) = lit(zero)
proof
  arbitrary a:Nat, y:Nat
  assume a_y: a < y
  expand add_div | lit | operator/
  replace (apply eq_true to a_y).
end
auto lit_add_div_zero

// Nothing is strictly less than literal zero (boolean form).
theorem lit_less_zero_false: all x:Nat. (x < lit(zero)) = false
proof
  arbitrary x:Nat
  expand lit.
end

auto lit_less_zero_false

// Literal zero is `≤` everything (boolean form).
theorem lit_zero_less_equal_true: all x:Nat. (lit(zero) ≤ x) = true
proof
  arbitrary x:Nat
  expand lit.
end

auto lit_zero_less_equal_true

// Squaring expressed as the literal exponent two.
theorem lit_expt_two : all n : Nat.
  n ^ ℕ2 = n * n
proof
  arbitrary n:Nat
  expand lit
  expt_two
end

// One raised to any power is one (literal form).
theorem lit_one_expt : all n :Nat.
  ℕ1 ^ n = ℕ1
proof
  arbitrary n:Nat
  expand lit
  one_expt
end

auto lit_one_expt