import Option
import Base

union Nat {
  zero
  suc(Nat)
}

recursive operator +(Nat,Nat) -> Nat {
  operator +(0, m) = m
  operator +(suc(n), m) = suc(n + m)
}

recursive operator *(Nat,Nat) -> Nat {
  operator *(0, m) = 0
  operator *(suc(n), m) = m + (n * m)
}

recursive expt(Nat, Nat) -> Nat {
  expt(0, n) = 1
  expt(suc(p), n) = n * expt(p, n)
}

fun operator ^(a : Nat, b : Nat)  {
  expt(b, a)
}

recursive max(Nat,Nat) -> Nat {
  max(zero, n) = n
  max(suc(m'), n) =
    switch n {
      case zero { suc(m') }
      case suc(n') { suc(max(m',n')) }
    }
}

recursive min(Nat,Nat) -> Nat {
  min(zero, n) = zero
  min(suc(m'), n) =
    switch n {
      case zero { zero }
      case suc(n') { suc(min(m',n')) }
    }
}

fun pred(n : Nat) {
  switch n {
    case 0 { 0 }
    case suc(n') { n' }
  }
}

recursive operator -(Nat,Nat) -> Nat {
  operator -(0, m) = 0
  operator -(suc(n), m) =
    switch m {
      case 0 { suc(n) }
      case suc(m') { n - m' }
    }
}

recursive operator ≤(Nat,Nat) -> bool {
  operator ≤(0, m) = true
  operator ≤(suc(n'), m) =
    switch m {
      case 0 { false }
      case suc(m') { n' ≤ m' }
    }
}

fun operator < (x:Nat, y:Nat) {
  suc(x) ≤ y
}

fun operator > (x:Nat, y:Nat) {
  y < x
}

fun operator ≥ (x:Nat, y:Nat) {
  y ≤ x
}


recursive summation(Nat, Nat, fn Nat->Nat) -> Nat {
  summation(0, begin, f) = 0
  summation(suc(k), begin, f) = f(begin) + summation(k, suc(begin), f)
}

recursive iterate<T>(Nat, T, fn T -> T) -> T {
  iterate(0, init, f) = init
  iterate(suc(n), init, f) = f(iterate(n, init, f))
}

recursive pow2(Nat) -> Nat {
  pow2(0) = 1
  pow2(suc(n')) = 2 * pow2(n')
}

private recursive div2_helper(Nat, bool) -> Nat {
  div2_helper(0, b) = 0
  div2_helper(suc(n'), b) =
    if b then div2_helper(n', not b)
    else suc(div2_helper(n', not b))
}

private fun div2(n : Nat) {
  div2_helper(n, true)
}

private fun div2_aux(n : Nat) {
  div2_helper(n, false)
}

recursive equal(Nat, Nat) -> bool {
  equal(0, n) =
    switch n {
      case 0 { true }
      case suc(n') { false }
    }
  equal(suc(m'), n) =
    switch n {
      case 0 { false }
      case suc(n') { equal(m', n') }
    }
}

recursive dist(Nat, Nat) -> Nat {
  dist(0, n) = n
  dist(suc(m), n) =
    switch n {
      case 0 {
        suc(m)
      }
      case suc(n') {
        dist(m, n')
      }
    }
}

/*
 Properties of Addition
 */

theorem zero_add: all n:Nat.
  0 + n = n
proof
  arbitrary n:Nat
  conclude 0 + n = n by definition operator+
end

theorem add_zero: all n:Nat.
  n + 0 = n
proof
  induction Nat
  case 0 {
    conclude 0 + 0 = 0   by definition operator+
  }
  case suc(n') suppose IH: n' + 0 = n' {
    equations
      suc(n') + 0 = suc(n' + 0)  by definition operator+
              ... = suc(n')      by replace IH
  }
end

theorem suc_add: all m:Nat, n:Nat.
  suc(m) + n = suc(m + n)
proof
  arbitrary m:Nat, n:Nat
  definition operator+
end

theorem suc_one_add: all n:Nat.
  suc(n) = 1 + n
proof
  arbitrary n:Nat
  equations
    suc(n) =# suc(0 + n) #      by definition operator+
       ... = suc(0) + n         by symmetric suc_add[0, n]
end

theorem one_add_suc: all n:Nat.
  1 + n = suc(n)
proof
  arbitrary n:Nat
  symmetric suc_one_add[n]
end

theorem not_one_add_zero: all n:Nat.
  not (1 + n = 0)
proof
  arbitrary n:Nat
  definition operator+
end

theorem add_suc: all m:Nat. all n:Nat.
  m + suc(n) = suc(m + n)
proof
  induction Nat
  case 0 {
    arbitrary n : Nat
    conclude 0 + suc(n) = suc(0 + n)  by evaluate
  }
  case suc(n') suppose IH {
    arbitrary n : Nat
    equations
      suc(n') + suc(n) = suc(n' + suc(n))  by evaluate
                   ... = suc(suc(n' + n))  by replace IH
                   ... = suc(suc(n') + n)  by evaluate
  }
end

theorem add_commute: all n:Nat. all m:Nat.  n + m = m + n
proof
  induction Nat
  case 0 {
    arbitrary m : Nat
    equations  0 + m = m      by evaluate
                 ... = m + 0  by symmetric add_zero[m]
  }
  case suc(n') suppose IH {
    arbitrary m : Nat
    equations suc(n') + m = suc(n' + m)     by evaluate
                      ... = suc(m + n')     by replace IH
                      ... = # m + suc(n') # by replace add_suc
  }
end

theorem one_add: all m:Nat.  1 + m = suc(m)
proof
  arbitrary m:Nat
  definition 2 * operator+
end

theorem add_one: all m:Nat.  m + 1 = suc(m)
proof
  arbitrary m:Nat
  equations
    m + 1 = 1 + m       by add_commute[m][1]
      ... = suc(m)      by one_add[m]
end

theorem add_assoc: all m:Nat, n:Nat, o:Nat.
  (m + n) + o = m + (n + o)
proof
  induction Nat
  case 0 {
    arbitrary n:Nat, o:Nat
    conclude (0 + n) + o = 0 + (n + o)   by evaluate
  }
  case suc(m') suppose IH {
    arbitrary n:Nat, o:Nat
    equations
      (suc(m') + n) + o = suc((m' + n) + o)  by evaluate
                    ... = suc(m' + (n + o))  by replace IH
                    ... = suc(m') + (n + o)  by evaluate
  }
end

associative operator+ in Nat

theorem assoc_add: all m:Nat, n:Nat, o:Nat.
  m + (n + o) = (m + n) + o
proof
  arbitrary m:Nat, n:Nat, o:Nat
  symmetric add_assoc
end

theorem add_both_sides_of_equal: all x:Nat. all y:Nat, z:Nat.
  x + y = x + z ⇔ y = z
proof
  induction Nat
  case 0 {
    arbitrary y:Nat, z:Nat
    evaluate
  }
  case suc(x') suppose IH {
    arbitrary y:Nat, z:Nat
    suffices __ by definition operator+
    have A: suc(x' + y) = suc(x' + z) ⇔ (x' + y = x' + z)
      by { assume seq injective suc seq } , { assume eq replace eq }
    have B: ((x' + y = x' + z) ⇔ (y = z)) by IH[y,z]
    conclude ((suc(x' + y) = suc(x' + z)) ⇔ (y = z))
      by apply iff_trans[suc(x' + y) = suc(x' + z), x' + y = x' + z, y = z]
         to A, B
  }
end

// left_cancel is obsolete, remove soon.
// Use add_both_sides_of_equal instead.
theorem left_cancel: all x:Nat. all y:Nat, z:Nat.
  if x + y = x + z then y = z
proof
  induction Nat
  case 0 {
    arbitrary y:Nat, z:Nat
    suppose prem: 0 + y = 0 + z
    equations   y = 0 + y      by evaluate
              ... = 0 + z      by prem
              ... = z          by evaluate
  }
  case suc(x') suppose IH: all y:Nat, z:Nat. if x' + y = x' + z then y = z {
    arbitrary y:Nat, z:Nat
    suppose prem: suc(x') + y = suc(x') + z
    suffices y = z by .
    apply IH[y,z] to {
      suffices x' + y = x' + z by .
      injective suc
      conclude suc(x' + y) = suc(x' + z)  by evaluate in prem
    }
  }
end

theorem add_to_zero: all n:Nat. all m:Nat.
  if n + m = 0
  then n = 0 and m = 0
proof
  induction Nat
  case 0 {
    arbitrary m:Nat
    suppose zmz
    have: m = 0
      by definition operator + in zmz
    replace (recall m = 0)
  }
  case suc(n') suppose IH {
    arbitrary m:Nat
    suppose snmz: suc(n') + m = 0
    conclude false
        by definition operator + in snmz
  }
end

/*
 Properties of Subtraction
 */
 
theorem zero_sub: all x:Nat. 0 - x = 0
proof
  evaluate
end

theorem sub_cancel: all n:Nat. n - n = 0
proof
  induction Nat
  case 0 {
    conclude 0 - 0 = 0   by definition operator-
  }
  case suc(n') assume IH: n' - n' = 0 {
    equations
      suc(n') - suc(n') = n' - n'    by definition operator-
                    ... = 0          by IH
  }
end

theorem sub_zero: all n:Nat.
  n - 0 = n
proof
  induction Nat
  case 0 {
    conclude 0 - 0 = 0   by definition operator-
  }
  case suc(n') suppose IH {
    conclude suc(n') - 0 = suc(n')  by definition operator-
  }
end

/*
 Properties of pred
*/

theorem pred_one: pred(suc(0)) = 0
proof
 definition pred
end

theorem pred_suc_n: all n:Nat. pred(suc(n)) = n
proof
  evaluate
end

theorem sub_one_pred : all x : Nat. x - 1 = pred(x)
proof
 induction Nat
 case zero {
   definition {pred, operator-}
 }
 case suc(x') {
   definition { pred, operator- }
   and replace sub_zero
 }
end

/*
 Properties of Addition and Subtraction
 */

theorem add_sub_identity: all m:Nat. all n:Nat. 
  (m + n) - m = n
proof
  induction Nat
  case 0 {
    arbitrary n:Nat
    equations   (0 + n) - 0 = n - 0    by replace zero_add
                        ... = n        by sub_zero[n]
  }
  case suc(m') suppose IH {
    arbitrary n:Nat
    equations  (suc(m') + n) - suc(m')
             = suc(m' + n) - suc(m')      by replace suc_add
         ... = (m' + n) - m'              by definition operator-
         ... = n                          by IH[n]
  }
end

theorem sub_sub_eq_sub_add : all x : Nat. all y:Nat. all z:Nat.
  (x - y) - z = x - (y + z)
proof
  induction Nat
  case zero { definition operator- }
  case suc(x') suppose IH{
    arbitrary y :Nat
    switch y {
      case zero {
        arbitrary z : Nat
        replace sub_zero | zero_add
      }
      case suc(y')  {
        arbitrary x : Nat
        switch x {
          case zero {
            replace sub_zero | add_zero
          }
          case suc(z')  {
            suffices  (x' - y') - suc(z') = x' - (y' + suc(z'))
              by definition { operator+, operator- }
            IH[y'][suc(z')]
          }
        }
      }
    }
  }
end

theorem sub_order : all x : Nat, y : Nat, z : Nat.
  (x - y) - z = (x - z) - y
proof
  arbitrary x : Nat, y : Nat, z : Nat
  equations  (x - y) - z = x - (y + z)   by sub_sub_eq_sub_add
                     ... = x - (z + y)   by replace add_commute
                     ... = #(x - z) - y# by replace sub_sub_eq_sub_add
end

/*
 Properties of Multiplication
*/

theorem zero_mult: all n:Nat.
  0 * n = 0
proof
  arbitrary n:Nat
  definition operator*
end
  
theorem mult_zero: all n:Nat.
  n * 0 = 0
proof
  induction Nat
  case 0 {
    conclude 0 * 0 = 0   by definition operator*
  }
  case suc(n') suppose IH {
    equations  suc(n') * 0 = 0 + n' * 0      by definition operator*
                       ... = n' * 0          by zero_add[n'*0]
                       ... = 0               by IH
  }
end

theorem suc_mult: all m:Nat, n:Nat.
  suc(m) * n = n + m * n
proof
  arbitrary m:Nat, n:Nat
  definition operator*
end

theorem mult_suc: all m:Nat. all n:Nat.
  m * suc(n) = m + m * n
proof
  induction Nat
  case 0 {
    arbitrary n:Nat
    equations   0 * suc(n) = 0            by zero_mult[suc(n)]
                       ... = 0 * n        by symmetric zero_mult[n]
                       ... = 0 + 0 * n    by symmetric zero_add[0*n]
  }
  case suc(m') suppose IH: all n:Nat. m' * suc(n) = m' + m' * n {
    arbitrary n:Nat
    suffices suc(n + m' * suc(n)) = suc(m' + (n + m' * n))
        by definition operator* | 2*operator+
    equations   suc(n + m' * suc(n))
              = suc(n + m' + m' * n)       by replace IH
          ... = suc(m' + n + m' * n)       by replace add_commute[n][m']
  }
end

theorem mult_commute: all m:Nat. all n:Nat.
  m * n = n * m
proof
  induction Nat
  case 0 {
    arbitrary n:Nat
    equations    0 * n = 0          by zero_mult[n]
                   ... = n * 0      by symmetric mult_zero[n]
  }
  case suc(m') suppose IH: all n:Nat. m' * n = n * m' {
    arbitrary n:Nat
    equations    suc(m') * n
               = n + m' * n     by definition operator*
           ... = n + (n * m')   by replace IH
           ... = n * suc(m')    by symmetric mult_suc[n][m']
  }
end

theorem one_mult: all n:Nat.
  1 * n = n
proof
  arbitrary n:Nat
  equations     1 * n = n + 0 * n    by suc_mult[0,n]
                  ... = n + 0        by replace zero_mult
                  ... = n            by add_zero[n]
end
  
theorem mult_one: all n:Nat.
  n * 1 = n
proof
  arbitrary n:Nat
  equations    n * 1 = 1 * n    by mult_commute[n][1]
                 ... = n        by one_mult[n]
end


theorem mult_to_zero : all n :Nat, m : Nat.
  if m * n = 0 then m = 0 or n = 0
proof
  arbitrary n : Nat, m :Nat
  switch n {
    case 0 { . }
    case suc(n') assume eq_sn_t {
      switch m {
        case 0 { . }
        case suc(m') assume eq_sm_t {
          evaluate
        }
      }
    }
  }
end

theorem one_mult_one : all x : Nat, y : Nat.
  if x * y = 1 then x = 1 and y = 1
proof
  arbitrary x : Nat, y : Nat
  switch x {  
    case 0 {
    definition operator*
  }
  case suc(x') suppose IH {
    switch y {
    case 0 {
      rewrite mult_zero[suc(x')]
    }
    case suc(y') {
      suffices (if suc(y' + x' * suc(y')) = 1 then (suc(x') = 1 and suc(y') = 1)) 
        by definition { operator*, operator+ }
      suppose prem
      have blah : y' + x' * suc(y') = 0 
        by injective suc
           prem
      have y'_zero : y' = 0 by apply add_to_zero to blah
      have x'sy'_zero : x' * suc(y') = 0 by apply add_to_zero to blah
      have x'_zero : x' = 0
        by switch x' {case 0 {
          .
        }
        case suc(n') suppose x_sn' {
          definition { operator*, operator+ } in rewrite x_sn' in x'sy'_zero
        }}
        rewrite x'_zero | y'_zero
    }}
  }}
end

theorem two_mult: all n:Nat.
  2 * n = n + n
proof
  arbitrary n:Nat
  equations   2 * n = n + 1 * n    by suc_mult[1,n]
                ... = n + n        by replace one_mult
end

theorem dist_mult_add:
  all a:Nat, x:Nat, y:Nat.
  a * (x + y) = a * x + a * y
proof
  induction Nat
  case zero {
    arbitrary x:Nat, y:Nat
    equations   0 * (x + y)
              = 0                     by zero_mult[x+y]
          ... = 0 + 0                 by symmetric add_zero[0]
          ... =# 0 * x + 0 * y #      by replace zero_mult
  }
  case suc(a') suppose IH {
    arbitrary x:Nat, y:Nat
    suffices (x + y) + a' * (x + y) = (x + a' * x) + (y + a' * y)
        by definition operator *
    equations
            (x + y) + a' * (x + y)
          = x + y + a'*x + a'*y           by replace IH
      ... = x + a'*x + y + a'*y           by replace add_commute[y, a'*x]
  }
end

theorem dist_mult_add_right:
  all x:Nat, y:Nat, a:Nat.
  (x + y) * a = x * a + y * a
proof
  arbitrary x:Nat, y:Nat, a:Nat
  equations
  (x + y) * a = a * (x + y)         by replace mult_commute
          ... = a * x + a * y       by dist_mult_add[a][x,y]
          ... = x * a + y * a       by replace mult_commute
end
  
theorem mult_assoc: all m:Nat. all n:Nat, o:Nat.
  (m * n) * o = m * (n * o)
proof
  induction Nat
  case 0 {
    arbitrary n:Nat, o:Nat
    equations   (0 * n) * o = 0 * o         by replace zero_mult
                        ... = 0             by zero_mult[o]
                        ... = 0 * (n * o)   by symmetric zero_mult[n*o]
  }
  case suc(m') suppose IH: all n:Nat, o:Nat. (m' * n) * o = m' * (n * o) {
    arbitrary n:Nat, o:Nat
    equations
          (suc(m') * n) * o
        = (n + m' * n) * o          by definition operator*
    ... = n * o + (m' * n) * o      by dist_mult_add_right[n, m'*n, o]
    ... = n * o + m' * (n * o)      by replace IH
    ... =# suc(m') * (n * o) #      by definition operator*
  }
end

associative operator* in Nat

theorem mult_right_cancel : all m : Nat, n : Nat, o : Nat.
  if m * suc(o) = n * suc(o) then m = n
proof
  induction Nat
  case 0 {
    arbitrary n:Nat, o:Nat
    switch n {
      case 0 { . }
      case suc(n') {
        assume contra: 0 * suc(o) = suc(n') * suc(o)
        conclude false by evaluate in contra
      }
    }
  }
  case suc(m') assume IH {
    arbitrary n:Nat, o:Nat
    switch n {
      case 0 {
        assume contra: suc(m') * suc(o) = 0 * suc(o)
        conclude false by evaluate in contra
      }
      case suc(n') {
        assume prem: suc(m') * suc(o) = suc(n') * suc(o)
        have prem2: suc(o) + m' * suc(o) = suc(o) + n' * suc(o)
          by definition operator* in prem
        have prem3: m' * suc(o) = n' * suc(o)
          by apply left_cancel to prem2
        have: m' = n' by apply IH to prem3
        conclude suc(m') = suc(n') by replace recall m' = n'
      }
    }
  }
end

theorem mult_left_cancel : all m : Nat, a : Nat, b : Nat.
  if suc(m) * a = suc(m) * b then a = b
proof
  arbitrary m:Nat, a:Nat, b:Nat
  assume prem: suc(m) * a = suc(m) * b
  have prem2: a * suc(m) = b * suc(m)  by rewrite mult_commute in prem
  conclude a = b by apply mult_right_cancel to prem2
end

/*
 Properties of Less-Than, Greater-Than, etc.
*/

theorem suc_less_equal_iff_less_equal_suc: all x:Nat, y:Nat.
  x ≤ y ⇔ suc(x) ≤ suc(y)
proof
  arbitrary x:Nat, y:Nat
  have sle : if x ≤ y then suc(x) ≤ suc(y)
    by suppose prem
      suffices x ≤ y by definition operator≤
      prem
  have els : if suc(x) ≤ suc(y) then x ≤ y
    by suppose prem
      definition operator≤ in prem
  sle, els
end

theorem less_suc_iff_suc_less: all x:Nat, y:Nat.
  x < y ⇔ suc(x) < suc(y)
proof
  arbitrary x:Nat, y:Nat
  have ls : if x < y then suc(x) < suc(y)
    by suppose x_l_y
      suffices suc(x) ≤ y by definition {operator<, operator≤}
      definition operator< in x_l_y
  have sl : if suc(x) < suc(y) then x < y
    by suppose sx_l_sy
      suffices suc(x) ≤ y      by definition operator<
      apply suc_less_equal_iff_less_equal_suc[suc(x), y]
      to definition operator< in sx_l_sy
  ls, sl
end

theorem not_less_zero:
  all x:Nat. not (x < 0)
proof
  definition {operator<, operator≤}
end       

theorem less_equal_implies_less_or_equal:
  all x:Nat. all y:Nat.
  if x ≤ y then x < y or x = y
proof
  induction Nat
  case 0 {
    arbitrary y:Nat
    switch y {
      case 0 {
        .
      }
      case suc(y') {
        suppose _
        suffices suc(0) ≤ suc(y')    by definition operator<
        suffices 0 ≤ y'              by definition operator≤
        definition operator≤
      }
    }
  }
  case suc(x') suppose IH {
    arbitrary y:Nat
    suppose sx_le_y
    switch y {
      case 0 suppose yz {
        conclude false  by definition operator≤ in replace yz in sx_le_y
      }
      case suc(y') suppose y_sy {
        have: x' ≤ y'
          by definition operator≤ in replace y_sy in sx_le_y
        have: x' < y' or x' = y'
          by IH[y'], recall x' ≤ y'
        cases (recall x' < y' or x' = y')
        case x_l_y {
          have sx_l_sy: suc(x') < suc(y')
            by apply less_suc_iff_suc_less to x_l_y
          conclude (suc(x') < suc(y') or suc(x') = suc(y'))
            by sx_l_sy
        }
        case x_y {
          have sx_sy: suc(x') = suc(y')
            by replace x_y
          conclude (suc(x') < suc(y') or suc(x') = suc(y'))
            by sx_sy
        }
      }
    }
  }
end

theorem less_equal_not_equal_implies_less:
  all x:Nat, y:Nat.
  if x ≤ y and not (x = y) then x < y
proof
  arbitrary x:Nat, y:Nat
  assume prem: x ≤ y and not (x = y)
  have LE: x < y or x = y by apply less_equal_implies_less_or_equal[x,y] to prem
  cases LE
  case less { less }
  case eq { conclude false by apply prem to eq }
end

theorem less_implies_less_equal:
  all x:Nat. all y:Nat.
  if x < y then x ≤ y
proof
  induction Nat
  case zero {
    arbitrary y:Nat
    suppose _
    conclude 0 ≤ y  by definition operator ≤
  }
  case suc(x') suppose IH {
    arbitrary y:Nat
    suppose sx_y: suc(x') < y
    have ssx_y: suc(suc(x')) ≤ y  by definition operator < in sx_y
    switch y {
      case zero suppose yz {
        conclude false  by definition operator ≤ in (replace yz in ssx_y)
      }
      case suc(y') suppose EQ : y = suc(y') {
        have ssx_sy: suc(suc(x')) ≤ suc(y')  by replace EQ in ssx_y
        have: x' < y'
            by suffices suc(x') ≤ y'  by definition operator <
               definition operator ≤ in ssx_sy
        suffices suc(x') ≤ suc(y')   by .
        suffices x' ≤ y'   by definition operator ≤          
        IH[y'], recall x' < y'
      }
    }
  }
end

theorem less_equal_refl: all n:Nat. n ≤ n
proof
  induction Nat
  case 0 { conclude 0 ≤ 0  by evaluate }
  case suc(n') suppose IH {
    suffices n' ≤ n' by evaluate
    IH
  }
end

theorem equal_implies_less_equal: all x:Nat, y:Nat.
  if x = y then x ≤ y
proof
  arbitrary x:Nat, y:Nat
  suppose x_y
  suffices y ≤ y  by replace x_y
  less_equal_refl[y]
end

theorem less_equal_antisymmetric:
  all x:Nat. all y:Nat. 
  if x ≤ y and y ≤ x
  then x = y
proof
  induction Nat
  case zero {
    arbitrary y:Nat
    suppose zy_yz: 0 ≤ y and y ≤ 0
    switch y {
      case zero { . }
      case suc(y') suppose y_suc {
        have sy_z: suc(y') ≤ 0 by replace y_suc in zy_yz
        conclude false by definition operator ≤ in sy_z
      }
    }
  }
  case suc(x') suppose IH {
    arbitrary y:Nat
    suppose sxy_ysx: suc(x') ≤ y and y ≤ suc(x')
    switch y {
      case zero suppose y_z {
        have: suc(x') ≤ 0 by replace y_z in sxy_ysx
        conclude false by definition operator ≤ in (recall suc(x') ≤ 0)
      }
      case suc(y') suppose y_suc {
        have: x' ≤ y' by evaluate in replace y_suc in sxy_ysx
        have: y' ≤ x' by evaluate in replace y_suc in sxy_ysx
        have: x' = y' by IH[y'], (recall x' ≤ y', y' ≤ x')
        conclude suc(x') = suc(y') by replace (recall x' = y')
      }
    }
  }
end

theorem less_equal_trans: all m:Nat. all n:Nat, o:Nat.
  if m ≤ n and n ≤ o then m ≤ o
proof
  induction Nat
  case 0 {
    arbitrary n:Nat, o:Nat
    suppose _
    conclude 0 ≤ o  by evaluate
  }
  case suc(m') suppose IH {
    arbitrary n:Nat, o:Nat
    suppose Prem: suc(m') ≤ n and n ≤ o
    have: suc(m') ≤ n  by Prem
    have: n ≤ o  by Prem
    switch n {
      case 0 suppose nz {
        have: suc(m') ≤ 0  by replace nz in (recall suc(m') ≤ n)
        conclude false  by evaluate in recall suc(m') ≤ 0
      }
      case suc(n') suppose: n = suc(n') {
        have sm_sn: suc(m') ≤ suc(n')
            by replace (recall n = suc(n')) in (recall suc(m') ≤ n)
        have: m' ≤ n'  by evaluate in sm_sn
        have: suc(n') ≤ o  by replace (recall n = suc(n')) in (recall n ≤ o)
        switch o {
          case 0 suppose: o = 0 {
            have: suc(n') ≤ 0  by replace (recall o = 0) in (recall suc(n') ≤ o)
            conclude false  by evaluate in recall suc(n') ≤ 0
          }
          case suc(o') suppose os {
            have: suc(n') ≤ suc(o')  by replace os in (recall suc(n') ≤ o)
            have: n' ≤ o'  by evaluate in recall suc(n') ≤ suc(o')
            suffices m' ≤ o' by evaluate
            IH[n',o'], recall m' ≤ n', n' ≤ o'
          }
        }
      }
    }
  }
end

// was not_less_less_equal
theorem not_less_implies_less_equal:
  all x: Nat. all y: Nat.
  if not (x < y) then y ≤ x
proof
  induction Nat
  case zero {
    arbitrary y: Nat
    suppose not_0_y: not (0 < y)
    switch y {
      case zero { definition operator ≤ }
      case suc(y') suppose ys {
        conclude false by apply (replace ys in not_0_y)
                          to (suffices 1 ≤ suc(y')   by definition operator <
                              definition {operator ≤,operator ≤})
      }
    }
  }
  case suc(x') suppose IH {
    arbitrary y: Nat
    suppose not_sx_y: not (suc(x') < y)
    switch y {
      case zero { definition operator ≤ }
      case suc(y') suppose ys {
        have not_x_y: not (x' < y')
          by (suppose x_y: x' < y'
            have sx_sy: suc(x') < suc(y')
              by suffices suc(suc(x')) ≤ suc(y')  by definition operator <
                 suffices suc(x') ≤ y'            by definition operator ≤
                 (definition operator < in x_y)
            have sx_y: suc(x') < y by (suffices suc(x') < suc(y')  by replace ys
                                       sx_sy)
            apply not_sx_y to sx_y)
        suffices y' ≤ x'  by definition operator ≤
        apply IH[y'] to not_x_y
      }
    }
  }
end

theorem less_irreflexive:  all x:Nat. not (x < x)
proof
  induction Nat
  case zero {
    suppose z_l_z: 0 < 0
    conclude false by evaluate in z_l_z
  }
  case suc(x') suppose IH: not (x' < x') {
    suppose sx_l_sx: suc(x') < suc(x')
    have x_l_x: x' < x' by apply less_suc_iff_suc_less to sx_l_sx
    conclude false by apply IH to x_l_x
  }
end

theorem less_not_equal: all x:Nat, y:Nat.
  if x < y then not (x = y)
proof
  arbitrary x:Nat, y:Nat
  suppose: x < y
  suppose: x = y
  have: y < y by replace (recall x = y) in recall x < y
  have: not (y < y) by less_irreflexive
  conclude false by recall y < y, not (y < y)
end

theorem greater_not_equal: all x:Nat, y:Nat.
  if x > y then not (x = y)
proof
  arbitrary x:Nat, y:Nat
  suppose: x > y
  suppose: x = y
  have: y > y  by replace (recall x = y) in (recall x > y)
  have: y < y  by definition operator> in recall y > y
  have: not (y < y) by less_irreflexive
  conclude false by recall y < y, not (y < y)
end

theorem trichotomy:
  all x:Nat. all y:Nat.
  x < y  or  x = y  or  y < x
proof
  induction Nat
  case zero {
    arbitrary y:Nat
    switch y {
      case zero { conclude 0 = 0 by . }
      case suc(y') {
        conclude 0 < suc(y') by definition operator < | 2 * operator ≤
      }
    }
  }
  case suc(x') suppose IH {
    arbitrary y:Nat
    switch y {
      case zero {
        conclude 0 < suc(x')
          by definition operator< | 2 * operator≤
      }
      case suc(y') {
        have IH': (x' < y' or x' = y' or y' < x') by IH[y']
        cases IH'
        case less { conclude suc(x') < suc(y')
            by suffices suc(suc(x')) ≤ suc(y')  by definition operator <
               suffices suc(x') ≤ y'            by definition operator ≤ 
               definition operator < in less
        }
        case x_eq_y { conclude suc(x') = suc(y')  by replace x_eq_y }
        case greater {
          conclude suc(y') < suc(x')
              by suffices suc(suc(y')) ≤ suc(x')   by definition operator <
                 suffices suc(y') ≤ x'             by definition operator ≤
                 definition operator < in greater
        }
      }
    }
  }
end
  
theorem trichotomy2:
  all y:Nat, x:Nat.
  if not (x = y) and not (x < y)
  then y < x
proof
  arbitrary y:Nat, x:Nat
  suppose prem: not (x = y) and not (x < y)
  cases trichotomy[x][y]
  case less: x < y {
    have not_less: not (x < y)  by prem
    conclude false  by apply not_less to less
  }
  case x_eq_y: x = y {
    have not_equal: not (x = y)  by prem
    conclude false  by apply not_equal to x_eq_y
  }
  case greater: y < x {
    conclude y <  x by greater
  }
end

lemma positive_1_and_2: 0 ≤ 1 and 0 ≤ 2
proof
  have one_pos: 0 ≤ 1 by definition operator ≤
  have two_pos: 0 ≤ 2 by definition operator ≤
  conclude 0 ≤ 1 and 0 ≤ 2 by one_pos, two_pos
end

lemma positive_2: 0 ≤ 2
proof
  conclude 0 ≤ 2 by positive_1_and_2
end

theorem dichotomy:  all x:Nat, y:Nat.  x ≤ y  or  y < x
proof
  arbitrary x:Nat, y:Nat
  have tri: x < y or x = y or y < x by trichotomy[x][y]
  cases tri
  case x_l_y: x < y {
    have x_le_y: x ≤ y by apply less_implies_less_equal[x][y] to x_l_y
    conclude x ≤ y or y < x by x_le_y
  }
  case x_eq_y: x = y {
    have x_le_y: x ≤ y by suffices y ≤ y  by replace x_eq_y
                          less_equal_refl[y]
    conclude x ≤ y or y < x by x_le_y
  }
  case y_l_x: y < x {
    conclude x ≤ y or y < x by y_l_x
  }
end

theorem zero_or_positive: all x:Nat. x = 0 or 0 < x
proof
  arbitrary x:Nat
  switch x {
    case zero {
      conclude true or 0 < 0 by .
    }
    case suc(x') {
      have z_l_sx: 0 < suc(x')
          by definition operator < | 2 * operator ≤
      conclude suc(x') = 0 or 0 < suc(x') by z_l_sx
    }
  }
end

theorem zero_le_zero: all x:Nat. if x ≤ 0 then x = 0
proof
  induction Nat
  case zero {
    suppose _
    .
  }
  case suc(x') {
    suppose prem: suc(x') ≤ 0
    conclude false by definition operator ≤ in prem
  }
end

theorem not_less_equal_iff_greater:
  all x:Nat, y:Nat.
  not (x ≤ y) ⇔ (y < x)
proof
  arbitrary x:Nat, y:Nat
  have nle_g : if not (x ≤ y) then y < x
    by suppose not_xy
    cases dichotomy[x,y]
    case x_le_y { apply not_xy to x_le_y }
    case y_l_x { y_l_x }
  have g_nle : if y < x then not (x ≤ y) 
    by suppose ylx
      have y_le_x : y ≤ x by apply less_implies_less_equal to ylx
      suppose label : x ≤ y
      have xy_a_yx : x ≤ y and y ≤ x by y_le_x, label
      have y_e_x:  y=x by symmetric (apply less_equal_antisymmetric to xy_a_yx)
      have x_ne_y: not (y = x) by apply less_not_equal to ylx
      replace y_e_x in x_ne_y
  nle_g, g_nle
end


theorem less_implies_not_greater:
  all x:Nat. all y:Nat.
  if x < y then not (y < x)
proof
  induction Nat
  case zero {
    arbitrary y:Nat
    suppose zero_less_y
    suppose y_less_zero
    conclude false by (definition {operator <, operator ≤} in y_less_zero)
  }
  case suc(x') suppose IH {
    arbitrary y:Nat
    suppose sx_less_y: suc(x') < y
    suppose y_less_sx: y < suc(x')
    switch y {
      case zero suppose y_eq_zero {
        conclude false by (definition {operator <, operator ≤} in
                       (replace y_eq_zero in sx_less_y))
      }
      case suc(y') suppose ys {
        have x_less_y: x' < y'  by {
          suffices __ by evaluate
          evaluate in replace ys in sx_less_y
        }
        have y_less_x: y' < x'  by {
          suffices __ by evaluate
          evaluate in replace ys in y_less_sx
        }
        conclude false by apply (apply IH[y'] to x_less_y) to y_less_x
      }
    }
  }
end

theorem not_less_equal_less_equal:
  all x:Nat, y:Nat.
  if not (x ≤ y) then y ≤ x
proof
  arbitrary x:Nat, y:Nat
  suppose not_xy
  have y_l_x: y < x  by apply not_less_equal_iff_greater to not_xy
  apply less_implies_less_equal to y_l_x
end

theorem not_zero_suc: all n:Nat.
  if not (n = 0)
  then some n':Nat. n = suc(n')
proof
  arbitrary n:Nat
  switch n {
    case 0 { . }
    case suc(n') {
      choose n'.
    }
  }
end

theorem positive_suc: all n:Nat.
  if 0 < n
  then some n':Nat. n = suc(n')
proof
  arbitrary n:Nat
  switch n {
    case 0 {
      suppose z_l_z: 0 < 0
      conclude false  by definition {operator<, operator≤} in z_l_z
    }
    case suc(n') {
      suppose z_l_sn: 0 < suc(n')
      choose n'.
    }
  }
end

/*
 Properties of Less-Than and Addition
 */

theorem less_equal_add: all x:Nat. all y:Nat.
  x ≤ x + y
proof
  induction Nat
  case 0 {
    arbitrary y:Nat
    conclude 0 ≤ 0 + y  by definition operator ≤
  }
  case suc(x') suppose IH {
    arbitrary y:Nat
    suffices x' ≤ x' + y   by definition {operator +, operator ≤}
    IH[y]
  }
end

theorem less_equal_add_left: all x:Nat, y:Nat.
  y ≤ x + y
proof
  arbitrary x:Nat, y:Nat
  suffices y ≤ y + x   by replace add_commute
  less_equal_add[y][x]
end

theorem less_equal_suc: all n:Nat.
  n ≤ suc(n)
proof
  arbitrary n:Nat
  definition 2 * operator+ in
  replace add_commute in
  less_equal_add[n][1]
end

theorem add_mono: all a:Nat, b:Nat, c:Nat, d:Nat.
  if a ≤ c and b ≤ d
  then a + b ≤ c + d
proof
  induction Nat
  case 0 {
    arbitrary b:Nat, c:Nat, d:Nat
    assume prem
    suffices __ by replace zero_add
    have bd: b ≤ d by prem
    have d_dc: d ≤ d + c by less_equal_add
    have d_cd: d ≤ c + d by replace add_commute in d_dc
    conclude b ≤ c + d by apply less_equal_trans to bd, d_cd
  }
  case suc(a') assume IH {
    arbitrary b:Nat, c:Nat, d:Nat
    assume prem
    have b_d: b ≤ d by prem
    switch c {
      case 0 assume cz {
        conclude false by evaluate in replace cz in prem
      }
      case suc(c') assume cs {
        have a_c: a' ≤ c'  by evaluate in replace cs in prem
        suffices __ by definition operator+ | operator≤
        conclude a' + b ≤ c' + d by apply IH to a_c, b_d
      }
    }
  }
end

theorem add_pos_nonneg : all a : Nat, b : Nat.
  if 0 < a then 0 < a + b
proof
  arbitrary a : Nat, b : Nat
  assume prem
  switch b {
    case 0 assume eq_z_t {
      suffices 0 < a by rewrite add_zero
      prem
    }
    case suc(b') assume eq_sn_t {
      suffices 0 < suc(a + b') by rewrite add_suc
      evaluate
    }
  }
end

theorem less_one_add: all n:Nat.
  0 < 1 + n
proof
  arbitrary n:Nat
  definition {operator<, operator≤, operator+, operator≤}
end

// less_equal_left_cancel
theorem add_both_sides_of_less_equal: all x:Nat. all y:Nat, z:Nat.
  x + y ≤ x + z ⇔ y ≤ z
proof
  induction Nat
  case 0 {
    definition operator+
  }
  case suc(x') suppose IH {
    suffices (all y:Nat, z:Nat. (x' + y ≤ x' + z ⇔ y ≤ z))
      by definition {operator+, operator≤}
    IH
  }
end

// was: less_left_cancel
theorem add_both_sides_of_less: all x:Nat, y:Nat, z:Nat.
  x + y < x + z ⇔ y < z
proof
  arbitrary x:Nat, y:Nat, z:Nat
  suffices suc(x + y) ≤ x + z ⇔ suc(y) ≤ z by definition operator<
  suffices (x + suc(y) ≤ x + z ⇔ suc(y) ≤ z) 
    by replace add_commute[x][y]
             | symmetric (definition operator+ in add_commute[x][suc(y)])
  add_both_sides_of_less_equal[x][suc(y), z]
end

theorem mult_mono_le : all n : Nat. all x : Nat, y : Nat.
  if x ≤ y then n * x ≤ n * y
proof
  induction Nat
  case zero {
    definition {operator*, operator≤}
  }
  case suc(n') suppose IH {
    arbitrary x:Nat, y:Nat
    suppose prem : x ≤ y
    suffices x + n' * x ≤ y + n' * y by definition operator*
    have nx_le_ny : n' * x ≤ n' * y by apply IH to prem
    have nyx_le_nyy : n' * y + x ≤ n' * y + y 
      by apply add_both_sides_of_less_equal[n'*y][x, y] to prem
    have xny_le_yny : x + n' * y ≤ y + n' * y
      by replace add_commute[n'*y][x]
               | add_commute[n'*y][y]
               in nyx_le_nyy
    have xnx_le_xny : x + n' * x ≤ x + n' * y
      by apply add_both_sides_of_less_equal[x][n'*x, n'*y] to nx_le_ny
    apply less_equal_trans to xnx_le_xny, xny_le_yny
  }
end


theorem mult_mono_le_r : all n : Nat. all x : Nat, y : Nat.
  if x ≤ y then x * n ≤ y * n
proof
  arbitrary n : Nat, x : Nat, y : Nat
  rewrite mult_commute[n, x] | mult_commute[n, y] in mult_mono_le[n, x, y]
end

/*
 Properties of Less-Than, Addition, and Subtraction
 */

theorem sub_add_assoc: all n:Nat. all l:Nat,m:Nat.
  if m ≤ n
  then l + (n - m) = (l + n) - m
proof
  induction Nat
  case 0 {
    arbitrary l:Nat, m:Nat
    suppose m_le_z: m ≤ 0
    suffices l + 0 = (l + 0) - m    by definition operator-
    suffices l = l - m              by replace add_zero
    have m_z: m = 0 by apply zero_le_zero to m_le_z
    replace m_z | sub_zero[l]
  }
  case suc(n') suppose IH {
    arbitrary l:Nat, m:Nat
    suppose m_le_sn
    switch m {
      case 0 {
        suffices l + suc(n') = (l + suc(n')) - 0  by definition {operator-}
        replace sub_zero
      }
      case suc(m') suppose m_sm {
        suffices l + (n' - m') = (l + suc(n')) - suc(m')
             by definition {operator-}
        suffices l + (n' - m') = suc(l + n') - suc(m')
             by replace add_suc
        suffices l + (n' - m') = (l + n') - m'
             by definition operator-
        have m_n: m' ≤ n'
          by definition operator ≤ in replace m_sm in m_le_sn
        apply IH[l, m'] to m_n
      }
    }
  }
end

theorem sub_suc_identity: all n:Nat.
   if 0 < n then suc(n - 1) = n
proof
   arbitrary n:Nat
   assume: 0 < n
   have X: 1 + (n - 1) = (1 + n) - 1 by apply sub_add_assoc[n,1,1] to definition operator< in recall 0 < n
   have Y: (1 + n) - 1 = n by add_sub_identity
   equations
     suc(n - 1) = #1 + (n - 1)# by definition 2*operator+
            ... = (1 + n) - 1   by apply sub_add_assoc[n,1,1] to definition operator< in recall 0 < n
            ... = n             by add_sub_identity
end

theorem sub_add_identity: all n:Nat. all m:Nat.
  if m ≤ n
  then m + (n - m) = n
proof
  induction Nat
  case 0 {
    arbitrary m:Nat
    suppose m_le_z
    suffices m + (0 - m) = 0  by .
    have m_z: m = 0 by apply zero_le_zero to m_le_z
    suffices 0 + (0 - 0) = 0   by replace m_z
    definition {operator-, operator+}
  }
  case suc(n') suppose IH {
    arbitrary m:Nat
    suppose m_le_sn
    suffices m + (suc(n') - m) = suc(n')  by .
    switch m {
      case 0 {
        conclude 0 + (suc(n') - 0) = suc(n') by definition {operator-,operator+}
      }
      case suc(m') suppose m_sm {
        suffices suc(m') + (suc(n') - suc(m')) = suc(n')  by .
        suffices suc(m' + (n' - m')) = suc(n')
          by definition {operator-,operator+}
        have m_n: m' ≤ n'  by definition operator≤ in replace m_sm in m_le_sn
        have IH_m: m' + (n' - m') = n' by apply IH[m'] to m_n
        replace IH_m
      }
    }
  }
end

theorem sub_right_cancel: all x:Nat, y:Nat, a:Nat.
  if x - a = y - a and a ≤ x and a ≤ y
  then x = y
proof
  arbitrary x:Nat, y:Nat, a:Nat
  assume prem
  have eq1: x - a = y - a by prem
  have eq2: (x - a) + a = (y - a) + a  by replace eq1
  have eq3: a + (x - a) = a + (y - a)  by replace add_commute in eq2
  conclude x = y by replace (apply sub_add_identity[x,a] to prem)
    | (apply sub_add_identity[y,a] to prem) in eq3
end
  
theorem less_equal_add_sub: all m:Nat. all n:Nat, o:Nat.
  if n ≤ m and m ≤ n + o
  then m - n ≤ o
proof
  induction Nat
  case 0 {
    arbitrary n:Nat, o:Nat
    suppose prem
    definition {operator -, operator ≤}
  }
  case suc(m') suppose IH {
    arbitrary n:Nat, o:Nat
    suppose prem
    switch n {
      case 0 suppose n_z {
        suffices suc(m') ≤ o  by definition operator -
        conclude suc(m') ≤ o
          by definition operator+ in replace n_z in prem
      }
      case suc(n') suppose n_sn {
        suffices m' - n' ≤ o  by definition operator-
        have n_m: n' ≤ m'
          by definition operator ≤ in replace n_sn
             in conjunct 0 of prem
        have m_no: m' ≤ n' + o
          by definition {operator ≤, operator +} in replace n_sn in 
             conjunct 1 of prem
        conclude m' - n' ≤ o  by apply IH[n',o] to n_m, m_no
      }
    }
  }
end

theorem sub_zero_iff_less_eq : all x : Nat, y : Nat. x ≤ y ⇔ x - y = 0
proof
  induction Nat 
  case 0 {
    conclude all y : Nat. 0 ≤ y ⇔ 0 - y = 0
      by definition {operator≤, operator-}
  }
  case suc(x') suppose IH {
    arbitrary y : Nat
    switch y {
      case 0 {
        suffices not (suc(x') ≤ 0) by definition operator-
        assume sx_le_z
        apply zero_le_zero[suc(x')] to sx_le_z
      }
      case suc(y') {
        suffices x' ≤ y' ⇔ x' - y' = 0
          by definition  {operator≤, operator-}
        IH[y']
      }
    }
  }
end

theorem sub_pos_iff_less: all x: Nat, y:Nat. y < x ⇔ 0 < x - y
proof
  induction Nat
  case 0 {
    arbitrary y:Nat
    have fwd: if y < 0 then 0 < 0 - y by
        definition {operator<, operator≤}
    have bkwd: if 0 < 0 - y then y < 0 by
        definition {operator-, operator<, operator≤}
    fwd, bkwd
  }
  case suc(x') assume IH {
    arbitrary y:Nat
    switch y {
      case 0 {
        have fwd: if 0 < suc(x') then 0 < suc(x') - 0
            by assume _ definition operator- | operator< | 2* operator≤
        have bkwd: if 0 < suc(x') - 0 then 0 < suc(x')
            by assume _ definition operator< | 2*operator≤
        fwd, bkwd
      }
      case suc(y') {
        have IH': y' < x' ⇔ 0 < x' - y' by IH[y']
        suffices suc(y') < suc(x') ⇔ 0 < x' - y' by definition operator-
        have syx_yx: suc(y') < suc(x') ⇔ y' < x'
            by apply iff_symm to less_suc_iff_suc_less[y',x']
        apply iff_trans[suc(y') < suc(x'), y' < x', 0 < x' - y']
        to syx_yx, IH'
      }
    }
  }
end

theorem le_exists_sub : all n : Nat, m : Nat.
  if n <= m then some x : Nat. m = n + x
proof
  arbitrary n : Nat, m :Nat
  assume prem
  choose m - n
  symmetric apply sub_add_identity[m, n] to prem
end

/*
 More Properties of Less
 */

theorem less_trans: all m:Nat, n:Nat, o:Nat.
  if m < n and n < o then m < o
proof
  arbitrary m:Nat, n:Nat, o:Nat
  suppose prem
  suffices suc(m) ≤ o   by definition operator <
  have _5: suc(m) ≤ suc(suc(m))
     by less_equal_suc[suc(m)]
  have _3: suc(suc(m)) ≤ suc(n) by
     suffices suc(m) ≤ n by definition operator≤
     definition operator < in prem
  have _2: suc(n) ≤ o   by definition operator < in prem
  have _4: suc(suc(m)) ≤ o
     by apply less_equal_trans to (_3, _2)
  conclude suc(m) ≤ o
     by apply less_equal_trans to (_5, _4)
end

theorem greater_any_zero: all x:Nat, y:Nat.
  if x < y
  then 0 < y
proof
  arbitrary x:Nat, y:Nat
  suppose x_l_y
  suffices 1 ≤ y  by definition operator<
  have sx_le_y: 1 + x ≤ y  by
    suffices suc(x) ≤ y  by definition 2*operator+
    definition operator< in x_l_y
  have one_le_sx: 1 ≤ 1 + x
    by less_equal_add[1][x]
  apply less_equal_trans to (one_le_sx, sx_le_y)
end

/*
 Properties of Multiplication and Subtraction
 */

// NOTE: This has to be after dichotomy, so it can't be with the other mult theorems
theorem dist_mult_sub : all x : Nat. all y : Nat, z : Nat.
  x * (y - z) = x * y - x * z
proof
  induction Nat
  case zero {
    arbitrary y:Nat, z:Nat
    suffices 0 = 0 - 0   by replace zero_mult
    definition operator-
  }
  case suc(n') suppose IH {
    arbitrary y:Nat, z:Nat
    suffices (n' * y - n' * z) + (y - z) = (y + n' * y) - (z + n' * z) 
      by definition operator*
         and replace IH | add_commute[(y - z)][(n' * y - n' * z)]
    cases dichotomy[z, y]
    case z_le_y: z ≤ y {
      have nz_le_ny : n'*z ≤n' * y
        by apply mult_mono_le[n', z, y] to z_le_y
      replace apply sub_add_assoc[y, (n' * y - n' * z) ,z] to z_le_y
            | add_commute[(n' * y - n' * z), y]
            | apply sub_add_assoc[n'*y, y, n'*z] to nz_le_ny
            | sub_sub_eq_sub_add[(y + n' * y), n' * z, z]
            | add_commute[n' * z, z]
    }
    case ylz: y < z {
      have y_le_z: y ≤ z by apply less_implies_less_equal[y, z] to ylz
      have ny_le_nz: n' * y ≤ n' * z by apply mult_mono_le[n', y, z] to y_le_z
      have zny_le_znz : z + n' * y ≤ z + n' * z
        by apply add_both_sides_of_less_equal[z, n'*y, n'*z] to ny_le_nz
      have nyy_le_nyz: n' * y + y ≤ n' * y + z
        by apply add_both_sides_of_less_equal[n'*y, y, z] to y_le_z
      have yny_le_zny : y + n' * y ≤ z + n' * y 
        by replace add_commute in nyy_le_nyz
      have yny_le_znz: y + n'*y ≤ z + n'*z
        by apply less_equal_trans to yny_le_zny, zny_le_znz
      suffices 0+0=0 
        by replace apply sub_zero_iff_less_eq to y_le_z
                 | apply sub_zero_iff_less_eq to ny_le_nz
                 | apply sub_zero_iff_less_eq to yny_le_znz
      add_zero[0]
    } 
  }
end


theorem mult_pos_nonneg : all a : Nat, b : Nat.
  if 0 < a and 0 < b then 0 < a * b
proof
  arbitrary a : Nat, b : Nat
  switch a {
    case 0 {
      evaluate
    }
    case suc(a') {
      assume prem
      suffices 0 < b + a' * b by definition operator*
      apply add_pos_nonneg[b, a'*b] to conjunct 1 of prem
    }
  }
end


theorem mult_lt_mono_l : all c : Nat, a : Nat, b : Nat.
  if c > 0 then (if a < b then a * c < b * c)
proof
  induction Nat
  case 0 {
    evaluate
  }
  case suc(c') assume IH {
    arbitrary a : Nat, b : Nat
    suppose sc_g_z
    suppose alb
    suffices  a + a * c' < b + b * c' by rewrite mult_suc | mult_suc
    switch c' > 0 {
      case true assume prop_t {
        have ac_l_bc : a * c' < b * c' by apply (rewrite prop_t in IH) to alb
        have step1 : a + a * c' < a + b * c' by apply add_both_sides_of_less[a, a*c'] to ac_l_bc
        have step2 : a + b * c' < b + b * c' by 
          suffices b * c' + a < b * c' + b 
            by rewrite add_commute[a, b * c'] | add_commute[b, b * c']
          apply add_both_sides_of_less[b * c'] to alb
        apply less_trans to step1, step2
      }
      case false assume prop_f {
        have cz : c' = 0 by rewrite (definition operator > in prop_f) in zero_or_positive[c']
        suffices a<b by rewrite cz | mult_zero | add_zero
        alb
      }
    }
  }
end

theorem mult_lt_mono_r :  all c : Nat, a : Nat, b : Nat.
  if 0 < c then (if a * c < b * c then a < b)
proof
  arbitrary c : Nat, a : Nat, b : Nat
  assume zlc
  assume ac_l_bc
  have cgz : c > 0 by 
    suffices __ by definition operator>
    zlc
  cases trichotomy[a, b]
  case : a < b {
    recall a < b
  }
  case aeb : a = b {
    apply less_irreflexive to rewrite aeb in ac_l_bc
  }
  case : b < a {
    have contra : b * c < a * c by 
      apply (apply mult_lt_mono_l[c, b, a] to cgz) to (recall b < a)
    apply (apply less_implies_not_greater[b*c, a*c] to contra) to ac_l_bc
  }
end


/*
  Properties of max
  */

lemma max_same: all x:Nat. max(x,x) = x
proof
  induction Nat
  case 0 {
    conclude max(0, 0) = 0  by definition max
  }
  case suc(x') suppose IH {
    suffices suc(max(x', x')) = suc(x')
      by definition max
    conclude suc(max(x', x')) = suc(x') by replace IH
  }
end

lemma max_suc: all x:Nat. max(suc(x), x) = suc(max(x,x))
proof
  induction Nat
  case zero {
    conclude max(suc(0), 0) = suc(max(0,0))  by definition max
  }
  case suc(x') suppose IH {
    equations
    # max(suc(suc(x')),suc(x')) #= suc(max(suc(x'),x'))
                                          by definition max
    ... = suc(suc(max(x',x')))            by replace IH
    ... =# suc(max(suc(x'),suc(x'))) #    by definition max
  }
end

lemma max_suc2: all x:Nat, y:Nat. max(suc(x), suc(y)) = suc(max(x,y))
proof
  arbitrary x:Nat, y:Nat
  switch x {
    case 0 {
      conclude max(1,suc(y)) = suc(max(0,y))   by definition 2*max
    }
    case suc(x') {
      switch y {
        case 0 {
          definition 2*max
        }
        case suc(y') {
          definition 2*max
        }
      }
    }
  }
end

theorem max_greater_right: all y:Nat, x:Nat. 
  y ≤ max(x, y)
proof
  induction Nat
  case 0 {
    arbitrary x:Nat
    definition operator ≤
  }
  case suc(y') suppose IH {
    arbitrary x:Nat
    switch x {
      case 0 {
        suffices suc(y') ≤ suc(y')  by definition max
        less_equal_refl[suc(y')]
      }
      case suc(x') {
        suffices suc(y') ≤ suc(max(x',y'))  by replace max_suc2
        suffices y' ≤ max(x',y')  by definition operator ≤
        IH[x']
      }
    }
  }
end

theorem max_greater_left: all x:Nat, y:Nat. 
  x ≤ max(x, y)
proof
  induction Nat
  case 0 {
    arbitrary y:Nat
    definition operator ≤
  }
  case suc(x') suppose IH {
    arbitrary y:Nat
    switch y {
      case 0 {
        suffices suc(x') ≤ suc(x')  by definition max
        conclude suc(x') ≤ suc(x')  by less_equal_refl[suc(x')]
      }
      case suc(y') {
        suffices x' ≤ max(x',y')  by definition max | operator ≤
        IH[y']
      }
    }
  }
end

theorem max_is_left_or_right: all x:Nat, y:Nat.
  max(x, y) = x or max( x
,y)=y
  proofinduction  Natcase0
    {arbitraryy:Nat
    definition max
  }
  case suc(x') suppose IH {
    arbitrary y:Nat
    switch y {
      case 0 {
        definition max
      }
      case suc(y') {
        cases IH[y']
        case m_x: max(x',y') = x' {
          suffices suc(max(x',y')) = suc(x')   by definition max
          replace m_x
        }
        case m_y: max(x',y') = y' {
          suffices suc(max(x',y')) = suc(y')   by definition max
          replace m_y
        }
      }
    }
  }
end

theorem zero_max: all x:Nat.
  max(0, x) = x
proof
  definition max
end

theorem max_zero: all x:Nat.
  max(x, 0) = x
proof
  induction Nat
  case 0 {
    conclude max(0, 0) = 0  by definition max
  }
  case suc(x') suppose IH {
    conclude max(suc(x'), 0) = suc(x')  by definition max
  }
end

theorem max_symmetric:  all x:Nat, y:Nat.
  max(x,y) = max(y,x)
proof
  induction Nat
  case 0 {
    arbitrary y:Nat
    suffices y = max(y, 0)  by definition max
    replace max_zero
  }
  case suc(x') suppose IH {
    arbitrary y:Nat
    switch y {
      case 0 {
        conclude max(suc(x'), 0) = max(0, suc(x'))
          by definition max
      }
      case suc(y') suppose y_suc {
        suffices suc(max(x', y')) = suc(max(y', x'))
            by replace max_suc2
        replace IH
      }
    }
  }
end

theorem max_assoc: all x:Nat, y:Nat,z:Nat.
  max(max(x, y), z) = max(x, max(y, z))
proof
  induction Nat
  case 0 {
    arbitrary y:Nat,z:Nat
    conclude max(max(0, y), z) = max(0, max(y, z))
        by definition max
  }
  case suc(x') suppose IH {
    arbitrary y:Nat,z:Nat
    switch y {
      case 0 {
        conclude max(max(suc(x'), 0), z) = max(suc(x'), max(0, z))
          by definition max
      }
      case suc(y') suppose y_suc {
        switch z {
          case 0 {
            conclude max(max(suc(x'), suc(y')), 0) = max(suc(x'), max(suc(y'), 0))
                by definition max
          }
          case suc(z') suppose z_suc {
            suffices suc(max(max(x', y'), z')) = suc(max(x', max(y', z')))
               by definition max
            replace IH
          }
        }
      }
    }
  }
end

theorem max_equal_greater_right: all x:Nat, y:Nat.
  if x ≤ y
  then max(x, y) = y
proof
  induction Nat
  case 0 {
    arbitrary y:Nat
    suppose _
    conclude max(0, y) = y   by definition max
  }
  case suc(x') suppose IH {
    arbitrary y:Nat
    suppose sx_le_y
    switch y for max {
      case 0 suppose y_z {
        conclude false  by definition operator≤ in
                           replace y_z in sx_le_y
      }
      case suc(y') suppose y_suc {
        have x_l_y: x' ≤ y'
            by definition operator≤ in replace y_suc in sx_le_y
        conclude suc(max(x', y')) = suc(y')
            by replace apply IH to x_l_y
      }
    }
  }
end

theorem max_equal_greater_left: all x:Nat, y:Nat.
  if y ≤ x
  then max(x, y) = x
proof
  arbitrary x:Nat
  arbitrary y:Nat
  suppose prem
  suffices max(y, x) = x   by replace max_symmetric
  apply max_equal_greater_right to prem
end

theorem max_less_equal: all x:Nat, y:Nat, z:Nat.
  if x ≤ z
  and y ≤ z
  then max(x, y) ≤ z
proof
  induction Nat
  case 0 {
    arbitrary y:Nat, z:Nat
    suppose prem
    suffices y ≤ z  by definition max
    prem
  }
  case suc(x') suppose IH {
    arbitrary y:Nat, z:Nat
    suppose prem
    switch y for max {
      case 0 {
        conclude suc(x') ≤ z by prem
      }
      case suc(y') suppose y_suc {
        suffices suc(max(x', y')) ≤ z   by .
        switch z {
          case 0 suppose z_zero {
            conclude false
                by definition operator≤ in
                   replace z_zero in prem
          }
          case suc(z') suppose z_suc {
            suffices max(x', y') ≤ z'  by definition operator≤
            have x_le_z: x' ≤ z' by
                definition operator≤ in replace z_suc in prem
            have y_le_z: y' ≤ z' by
                definition operator≤ in
                replace y_suc | z_suc in prem
            apply IH to x_le_z, y_le_z
          }
        }
      }
    }
  }
end


/*
 Odd and Even Numbers
 */

recursive parity(Nat, bool) -> bool {
  parity(0, b) = b
  parity(suc(n'), b) = parity(n', not b)
}

fun is_even(n : Nat) {
  parity(n, true)
}

fun is_odd(n : Nat) {
  parity(n, false)
}

fun Even(n : Nat) {
  some m:Nat. n = 2 * m
}

fun Odd(n : Nat) {
  some m:Nat. n = suc (2 * m)
}

theorem two_even: all n:Nat. Even(2*n)
proof
  arbitrary n:Nat
  suffices __ by definition Even
  choose n
  .
end

theorem one_two_odd: all n:Nat. Odd(1 + 2*n)
proof
  arbitrary n:Nat
  suffices __ by definition Odd
  choose n
  evaluate
end


theorem even_or_odd: all n:Nat. is_even(n) or is_odd(n)
proof
  induction Nat
  case 0 {
    conclude is_even(0) by definition {is_even, parity}
  }
  case suc(n') assume IH {
    cases IH
    case even {
      conclude is_odd(suc(n')) by
        suffices parity(n', true) by definition {is_odd, parity}
        definition is_even in even
    }
    case odd {
      conclude is_even(suc(n')) by
        suffices parity(n', false) by definition {is_even, parity}
        definition is_odd in odd
    }
  }
end


theorem addition_of_evens:
  all x:Nat, y:Nat.
  if Even(x) and Even(y) then Even(x + y)
proof
  arbitrary x:Nat, y:Nat
  suppose even_xy: Even(x) and Even(y)
  have even_x: some m:Nat. x = 2 * m by definition Even in even_xy
  have even_y: some m:Nat. y = 2 * m by definition Even in even_xy
  obtain a where x_2a: x = 2*a from even_x
  obtain b where y_2b: y = 2*b from even_y
  suffices some m:Nat. x + y = 2 * m  by definition Even
  choose a + b
  equations
        x + y
      = 2*a + 2*b       by replace x_2a | y_2b
  ... = #2 * (a + b)#   by replace dist_mult_add
end

theorem is_even_odd:
  all n:Nat.
  (if is_even(n) then Even(n))
  and (if is_odd(n) then Odd(n))
proof
  induction Nat
  case zero {
    have part1: if is_even(0) then Even(0)
      by suppose _
         conclude Even(0)
         by suffices some m:Nat. 0 = 2 * m  by definition Even
            choose 0
            evaluate
   have part2: if is_odd(0) then Odd(0)
     by suppose zero_odd
        conclude false by definition {is_odd, parity} in zero_odd
    part1, part2
  }
  case suc(n') suppose IH {
    have part1: (if is_even(suc(n')) then Even(suc(n'))) by
      (suppose suc_even: is_even(suc(n'))
      have odd_n: is_odd(n') by {
        suffices parity(n', false) by definition {is_odd}
        definition {is_even, parity} in suc_even
      }
      have Odd_n: Odd(n') by apply (conjunct 1 of IH) to odd_n
      obtain m where n_2m from definition Odd in Odd_n
      suffices some m':Nat. suc(n') = 2 * m'  by definition Even
      choose suc(m)
      suffices suc(suc(2 * m)) = 2 * suc(m)  by replace n_2m
      suffices suc(suc(m + (m + 0))) = suc(m + suc(m + 0))
          by definition 3 * operator* | 3 * operator+
      replace add_zero | add_suc)
    have part2: (if is_odd(suc(n')) then Odd(suc(n'))) by
      (suppose suc_odd: is_odd(suc(n'))
        have even_n: is_even(n') by {
          suffices parity(n', true) by definition is_even
          definition {is_odd, parity} in suc_odd
        }
        have Even_n: Even(n') by apply (conjunct 0 of IH) to even_n
        obtain m where n_2m from definition Even in Even_n
        suffices some m':Nat. suc(n') = suc(2 * m')  by definition Odd
        choose m
        replace n_2m)
    part1, part2
  }
end

theorem Even_or_Odd: all n:Nat. Even(n) or Odd(n)
proof
  arbitrary n:Nat
  cases even_or_odd[n]
  case even {
    conclude Even(n) by apply is_even_odd to even
  }
  case odd {
    conclude Odd(n) by apply is_even_odd to odd
  }
end

theorem odd_one_even: all n:Nat. if Odd(1 + n) then Even(n)
proof
  arbitrary n:Nat
  assume n1_odd
  obtain k where nk: 1 + n = suc(2 * k) from definition Odd in n1_odd
  have n2k: n = 2*k
    by apply add_both_sides_of_equal[1, n, 2*k] to (replace suc_one_add | add_zero in nk)
  suffices __ by definition Even
  choose k
  n2k
end

theorem even_one_odd: all n:Nat. if Even(1 + n) then Odd(n)
proof
  arbitrary n:Nat
  assume n1_even
  obtain k where nk: 1 + n = 2 * k from definition Even in n1_even
  suffices __ by definition Odd
  switch k {
    case 0 assume kz {
      conclude false by evaluate in replace kz in nk
    }
    case suc(k') assume ksk {
      have eq1: 1 + n = 1 + (1 + k' * 2) by {
        suffices __ by evaluate
        evaluate in definition operator* in replace ksk | mult_commute in nk
      }
      have n_eq: n = 1 + k' * 2 by apply add_both_sides_of_equal to eq1
      suffices __ by replace n_eq | suc_one_add | dist_mult_add | mult_one | add_zero
      choose k'
      replace two_mult
    }
  }
end

theorem Even_not_Odd: all n:Nat. Even(n) ⇔ not Odd(n)
proof
  induction Nat
  case 0 {
    suffices some m:Nat. 0 = 2 * m by definition Even | Odd
    choose 0
    conclude 0 = 2 * 0 by evaluate
  }
  case suc(n') assume IH {
		have fwd: if Even(suc(n')) then not Odd(suc(n')) by {
      assume prem: Even(suc(n'))
      assume contra: Odd(suc(n'))
      have en: Even(n') by apply odd_one_even to (replace suc_one_add in contra)
      have not_on: not Odd(n') by apply IH to en
      have on: Odd(n') by apply even_one_odd to (replace suc_one_add in prem)
      conclude false by apply not_on to on
    }
		have bkwd: if not Odd(suc(n')) then Even(suc(n')) by {
      assume prem: not Odd(suc(n'))
      have nen: not Even(n') by {
        assume en: Even(n')
        obtain k where n2k: n' = 2*k from definition Even in en
        have sn2k: suc(n') = suc(2*k) by replace n2k
        have osn: Odd(suc(n')) by {
          suffices __ by definition Odd
          choose k
          sn2k
        }
        conclude false by apply prem to osn
      }
      have nnon: not (not Odd(n'))
        by apply contrapositive[not Odd(n'), Even(n')] to IH, nen
      have on: Odd(n') by replace double_neg in nnon
      obtain k where ns2k: n' = suc (2 * k) from definition Odd in on
      suffices __ by definition Even and replace ns2k
      choose 1+k
      suffices __ by replace dist_mult_add | mult_one
      evaluate
    }
    fwd, bkwd
  }
end

/*
 Properties of Summation
 */

theorem summation_cong: all k : Nat. all f : fn Nat->Nat, g : fn Nat->Nat, s : Nat, t : Nat. 
  if (all i:Nat. if i < k then f(s + i) = g(t + i))
  then summation(k, s, f) = summation(k, t, g)
proof
  induction Nat
  case zero {
    arbitrary f:fn(Nat) -> Nat,g:fn(Nat) -> Nat,s:Nat,t:Nat
    suppose f_g
    definition summation
  }
  case suc(k') suppose IH {
    arbitrary f:fn(Nat) -> Nat,g:fn(Nat) -> Nat,s:Nat,t:Nat
    suppose f_g
    suffices summation(suc(k'),s,f) = summation(suc(k'),t,g)  by .
    suffices f(s) + summation(k',suc(s),f) = g(t) + summation(k',suc(t),g)
      by definition summation
    have f_g_s: f(s) = g(t) by
       replace add_zero in
       (apply f_g[0] to definition operator < | 2* operator ≤)
    have IH': summation(k',suc(s),f) = summation(k',suc(t),g)
      by apply IH[f,g,suc(s),suc(t)] 
         to arbitrary i:Nat suppose i_k: i < k'
            suffices f(suc(s + i)) = g(suc(t + i))  by evaluate
            have fsi_gtsi: f(s + suc(i)) = g(t + suc(i))
              by suffices suc(i) < suc(k') by f_g[suc(i)] 
                 apply less_suc_iff_suc_less to i_k
            replace add_suc  in fsi_gtsi
    replace f_g_s | IH'
  }
end

lemma summation_cong4: all k:Nat. all f : fn Nat->Nat, g : fn Nat->Nat, s :Nat. 
  if (all i:Nat. if s ≤ i and i < s + k then f(i) = g(i))
  then summation(k, s, f) = summation(k, s, g)
proof
  induction Nat
  case zero {
    arbitrary f : fn Nat->Nat, g : fn Nat->Nat, s :Nat
    suppose _
    definition summation
  }
  case suc(k') suppose IH {
    arbitrary f : fn Nat->Nat, g : fn Nat->Nat, s :Nat
    suppose f_g: all i:Nat. if s ≤ i and i < s + suc(k') then f(i) = g(i)
    suffices f(s) + summation(k',suc(s),f) = g(s) + summation(k',suc(s),g)
        by definition summation
    have f_g_s: f(s) = g(s) by {
      have s_s: s ≤ s by less_equal_refl[s]
      have s_sk: s < s + suc(k') by {
        suffices s ≤ s + k' by definition operator < | operator ≤ and replace add_suc
        less_equal_add[s][k']
      }
      apply f_g[s] to s_s, s_sk
    }
    have IH': summation(k',suc(s),f) = summation(k',suc(s),g) by {
      have IH_prem: all i:Nat. if (suc(s) ≤ i and i < suc(s) + k')
                               then f(i) = g(i) by
      {
        arbitrary i:Nat
        suppose ss_i_and_i_ss_k
        have s_i: s ≤ i by {
          apply less_implies_less_equal[s][i]
          to suffices suc(s) ≤ i  by definition operator <
          ss_i_and_i_ss_k
        } 
        have i_s_k: i < s + suc(k') by {
          suffices suc(i) ≤ suc(s + k')  by {
            suffices __ by evaluate
            replace add_suc
          }
          suffices i ≤ s + k' by evaluate
          evaluate in (conjunct 1 of ss_i_and_i_ss_k)
        }
        conclude f(i) = g(i) by apply f_g[i] to s_i, i_s_k
      }
      apply IH[f,g,suc(s)] to IH_prem
    }
    replace f_g_s | IH'
  }
end

theorem summation_suc: all k:Nat. all f : fn Nat->Nat, g : fn Nat->Nat, s :Nat. 
  if (all i:Nat. f(i) = g(suc(i)))
  then summation(k, s, f) = summation(k, suc(s), g)
proof
  arbitrary k:Nat
  arbitrary f : fn Nat->Nat, g : fn Nat->Nat, s :Nat
  suppose prem
  have sum_prem: (all i:Nat. (if i < k then f(s + i) = g(suc(s) + i))) by
      arbitrary i:Nat
      suppose i_less_k
      suffices f(s+i) = g(suc(s+i))  by definition operator+
      prem[s+i]
  apply summation_cong[k][f, g, s, suc(s)] to sum_prem
end

lemma summation_cong3: all k:Nat. all f : fn Nat->Nat, g : fn Nat->Nat, s :Nat, t :Nat. 
  if (all i:Nat. f(s + i) = g(t + i))
  then summation(k, s, f) = summation(k, t, g)
proof
  induction Nat
  case zero {
    arbitrary f : fn Nat->Nat, g : fn Nat->Nat, s :Nat, t :Nat
    suppose _
    definition summation
  }
  case suc(k') suppose IH {
    arbitrary f : fn Nat->Nat, g : fn Nat->Nat, s :Nat, t :Nat
    suppose f_g: all i:Nat. f(s + i) = g(t + i)
    suffices f(s) + summation(k',suc(s),f) = g(t) + summation(k',suc(t),g)  by definition summation
    have fs_gt: f(s) = g(t)   by replace add_zero in f_g[0]
    have all_f_g: all i:Nat. f(suc(s) + i) = g(suc(t) + i)
      by arbitrary i:Nat
         suffices f(suc(s + i)) = g(suc(t + i))  by definition operator +
         replace add_suc in f_g[suc(i)]
    equations
          f(s) + summation(k',suc(s),f)
        = g(t) + summation(k',suc(s),f)   by replace fs_gt
    ... = g(t) + summation(k',suc(t),g)   by replace (apply IH[f,g,suc(s),suc(t)] to all_f_g)
  }
end

theorem summation_add:
  all a:Nat. all b:Nat, s:Nat, t:Nat, f:fn Nat->Nat, g:fn Nat->Nat, h:fn Nat->Nat.
  if (all i:Nat. if i < a then g(s + i) = f(s + i))
  and (all i:Nat. if i < b then h(t + i) = f(s + a + i))
  then summation(a + b, s, f) = summation(a, s, g) + summation(b, t, h)
proof
  induction Nat
  case zero {
    arbitrary b:Nat, s:Nat, t:Nat, f:fn Nat->Nat, g:fn Nat->Nat, h:fn Nat->Nat
    suppose g_f_and_h_f
    suffices summation(b,s,f) = summation(b,t,h)  by definition { operator+, summation }
    apply summation_cong[b][f,h,s,t]
    to arbitrary i:Nat
       suppose i_b: i < b
       conclude f(s + i) = h(t + i)
       by definition operator+ in symmetric (apply (conjunct 1 of g_f_and_h_f)[i] to i_b)
  }
  case suc(a') suppose IH {
    arbitrary b:Nat, s:Nat, t:Nat, f:fn Nat->Nat, g:fn Nat->Nat, h:fn Nat->Nat
    suppose g_f_and_h_f
    suffices f(s) + summation(a' + b,suc(s),f) = (g(s) + summation(a',suc(s),g)) + summation(b,t,h)
        by definition {operator +, summation}
    have fs_gs: f(s) = g(s) by symmetric
        replace add_zero
        in apply (conjunct 0 of g_f_and_h_f)[0]
           to definition operator < | 2* operator ≤
    have IH': summation(a' + b,suc(s),f)
            = summation(a',suc(s),g) + summation(b,t,h)
      by have p1: all i:Nat. (if i < a' then g(suc(s) + i) = f(suc(s) + i))
           by arbitrary i:Nat suppose i_a: i < a'
              have i_sa : suc(i) < suc(a') by 
                apply less_suc_iff_suc_less to i_a
              replace add_suc | symmetric suc_add[s, i]
                in apply (conjunct 0 of g_f_and_h_f)[suc(i)] to i_sa
         have p2: all i:Nat. (if i < b then h(t + i) = f(suc(s) + (a' + i)))
           by arbitrary i:Nat suppose i_b: i < b
              suffices __ by definition 2*operator+
              definition operator+ in
              replace add_suc in
              apply (conjunct 1 of g_f_and_h_f)[i] to i_b
         apply IH[b,suc(s),t,f,g,h] to p1, p2
    replace fs_gs | IH' 
  }
end

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
  have A: (all i:Nat. (if i < n then f(s + i) = f(s + i))) by {
    arbitrary i:Nat assume: i < n .
  }
  have B: (all i:Nat. (if i < 1 then f((s + n) + i) = f(s + (n + i)))) by {
    arbitrary i:Nat assume: i < 1 .
  }
  have C: summation(n + 1, s, f) = summation(n, s, f) + summation(1, s+n, f)
    by apply summation_add[n,1,s,s+n,f,f,f] to A,B
  have D: summation(1, s + n, f) = f(s + n)
    by definition 2*summation and replace add_zero
  replace add_commute[1,n] | C | D
end

/*
 Properties of equal
*/
theorem equal_refl: all n:Nat. equal(n,n)
proof
  induction Nat
  case 0 {
    definition equal
  }
  case suc(n') suppose IH {
    suffices equal(n',n')  by definition equal
    IH
  }
end

theorem equal_complete_sound : all m:Nat. all n:Nat.
  m = n ⇔ equal(m, n)
proof
  induction Nat
  case 0 {
    arbitrary n:Nat
    switch n {
      case 0 { definition equal }
      case suc(n') { definition equal }
    }
  }
  case suc(m') suppose IH {
    arbitrary n:Nat 
    switch n {
      case 0 { definition 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 definition 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 definition equal in sm_sn
             have m_n : m' = n' by apply IH to e_m_n
             replace m_n
        right, left
      }
    }
  }
end

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

/*
 Properties of div2
 */

lemma div2_zero: div2(0) = 0
proof
  evaluate
end
 
lemma div2_add_2: all n:Nat.  div2(suc(suc(n))) = suc(div2(n))
proof
  arbitrary n:Nat
  definition {div2, div2_helper, div2_helper}
end

lemma div2_double: all n:Nat.
  div2(n + n) = n
proof
  induction Nat
  case 0 {
    definition {operator+, div2, div2_helper}
  }
  case suc(n') suppose IH {
    suffices div2(suc(n' + suc(n'))) = suc(n')  by definition operator+
    suffices div2(suc(suc(n' + n'))) = suc(n')  by replace add_suc
    suffices suc(div2(n' + n')) = suc(n')       by replace div2_add_2
    replace IH
  }
end

lemma div2_times2: all n:Nat.
  div2(2 * n) = n
proof
  arbitrary n:Nat
  suffices div2(n + (n + 0)) = n  by definition {operator*,operator*,operator*}
  suffices div2(n + n) = n        by replace add_zero
  div2_double[n]
end

lemma div2_suc_double: all n:Nat.
  div2(suc(n + n)) = n
proof
  induction Nat
  case 0 {
    definition {operator+, div2, div2_helper, div2_helper}
  }
  case suc(n') suppose IH {
    suffices suc(div2_helper(suc(n' + n'), true)) = suc(n')
      by definition {div2, div2_helper, operator+, div2_helper} and replace add_suc
    suffices suc(div2_helper(n' + n', false)) = suc(n')
      by definition div2_helper
    replace (definition {div2, div2_helper} in IH)
  }
end

lemma div2_suc_times2: all n:Nat.
  div2(suc(2 * n)) = n
proof
  arbitrary n:Nat
  suffices div2(suc(n + (n + 0))) = n  by definition {operator*,operator*,operator*}
  suffices div2(suc(n + n)) = n        by replace add_zero
  div2_suc_double[n]
end

lemma sub_div2: all n:Nat. n - div2(n) ≤ suc(div2(n))
proof
  arbitrary n:Nat
  cases Even_or_Odd[n]
  case even {
    obtain k where n_2k: n = 2 * k from definition Even in even
    suffices k ≤ suc(k) by replace n_2k | div2_times2[k] | two_mult[k] | add_sub_identity[k,k]
    less_equal_suc
  }
  case odd {
    obtain k where n_s2k: n = suc(2 * k) from definition Odd in odd
    suffices suc(k + k) - k ≤ suc(k) by replace n_s2k | div2_suc_times2[k] | two_mult[k]
    have eq_1: suc(k + k) = 1 + (k + k) by definition {operator+, operator+}
    suffices (1 + (k + k)) - k ≤ suc(k) by replace eq_1
    have k_kk: k ≤ k + k by less_equal_add
    have eq_2: (1 + (k + k)) - k = 1 + ((k + k) - k) by symmetric apply sub_add_assoc[k + k, 1, k] to k_kk
    suffices 1 + ((k + k) - k) ≤ suc(k) by replace eq_2
    suffices ((k + k) - k) ≤ k by definition {operator+, operator+, operator≤}
    suffices k ≤ k by replace add_sub_identity[k,k]
    less_equal_refl
  }
end

lemma sub_div2_pos: all n:Nat. if 0 < n then 0 < n - div2(n)
proof
  arbitrary n:Nat
  cases Even_or_Odd[n]
  case even {
    obtain k where n_2k: n = 2 * k from definition Even in even
    suffices if 0 < k + k then 0 < k by replace n_2k | div2_times2[k] | two_mult[k] | add_sub_identity[k,k]
    switch k {
      case 0 {
        conclude if 0 < 0 + 0 then 0 < 0
           by definition {operator +}
      }
      case suc(k') {
        assume _
        definition {operator<, operator≤, operator≤}
      }
    }
  }
  case odd {
    obtain k where n_s2k: n = suc(2 * k) from definition Odd in odd
    suffices if 0 < suc(k + k) then 0 < suc(k + k) - k by replace n_s2k | div2_suc_times2[k] | two_mult[k]
    assume _
    have eq_1: suc(k + k) = 1 + (k + k) by definition {operator+, operator+}
    suffices 0 < (1 + (k + k)) - k by replace eq_1
    have k_kk: k ≤ k + k by less_equal_add
    have eq_2: (1 + (k + k)) - k = 1 + ((k + k) - k) by symmetric apply sub_add_assoc[k + k, 1, k] to k_kk
    suffices 0 < 1 + ((k + k) - k) by replace eq_2
    definition {operator+, operator<, operator≤, operator≤}
  }
end

lemma div2_aux_pos_less: all n:Nat. if 0 < n then div2(n) < n and div2_aux(n) ≤ n
proof
  induction Nat
  case 0 {
    assume: 0 < 0
    conclude false by apply less_irreflexive to recall 0 < 0
  }
  case suc(n') assume IH {
    assume: 0 < suc(n')
    switch n' {
      case 0 {
        definition {div2, div2_aux, operator<, operator≤, div2_helper, div2_helper, operator≤}
      }
      case suc(n'') assume np_eq {
        have: 0 < n' by {
            suffices 0 < suc(n'') by replace np_eq
            definition {operator<, operator≤, operator≤}
        }
        have IH': div2(n') < n' and div2_aux(n') ≤ n' by apply IH to (recall 0 < n')
        suffices (div2_helper(n'', true) ≤ n'' and div2_helper(n'', false) ≤ suc(n''))
          by definition {div2, div2_aux, div2_helper, div2_helper, operator<, operator≤, operator≤}
        have _1: div2_helper(n'', true) ≤ n'' by {
          definition {div2_aux, div2_helper, operator≤} in
          replace np_eq in
          conjunct 1 of IH'
        }
        have _2: div2_helper(n'', false) ≤ suc(n'') by {
          have lt1: div2_helper(n'', false) ≤ n'' by {
            definition {div2, div2_helper, operator<, operator≤} in
            replace np_eq in
            conjunct 0 of IH'
          }
          have lt2: n'' ≤ suc(n'') by less_equal_suc
          apply less_equal_trans to lt1, lt2
        }
        _1, _2
      }
    }
  }
end

lemma div2_pos_less: all n:Nat. if 0 < n then div2(n) < n
proof
  div2_aux_pos_less
end

lemma div2_aux_mono: all x:Nat, y:Nat.
  if x ≤ y then div2(x) ≤ div2(y) and div2_aux(x) ≤ div2_aux(y)
proof
  induction Nat
  case 0 {
    arbitrary y:Nat
    assume _
    conclude div2(0) ≤ div2(y) and div2_aux(0) ≤ div2_aux(y)
        by definition {div2, div2_aux, div2_helper, operator≤}
  }
  case suc(x') assume IH {
    arbitrary y:Nat
    assume sx_y
    switch y {
      case 0 assume y_eq {
        conclude false by definition operator≤ in replace y_eq in sx_y
      }
      case suc(y') assume y_eq {
        suffices div2_helper(x', false) ≤ div2_helper(y', false)
             and div2_helper(x', true) ≤ div2_helper(y', true)
            by definition {div2, div2_aux, div2_helper, operator≤}
        have xy: x' ≤ y' by apply suc_less_equal_iff_less_equal_suc to replace y_eq in sx_y
        definition {div2, div2_aux} in apply IH[y'] to xy
      }
    }
  }
end

lemma div2_mono: all x:Nat, y:Nat.
  if x ≤ y then div2(x) ≤ div2(y)
proof
  div2_aux_mono
end

/*
 Properties of pow2
 */
 
theorem pow_positive: all n:Nat. 0 < pow2(n)
proof
  induction Nat
  case 0 {
    definition {pow2, operator<, operator≤, operator≤}
  }
  case suc(n') suppose IH {
    suffices 0 < 2 * pow2(n')  by definition pow2
    obtain pn' where pn_s: pow2(n') = suc(pn')
        from apply positive_suc[pow2(n')] to IH
    suffices 0 < 2 * suc(pn')  by replace pn_s
    suffices 0 < suc(pn') + (suc(pn') + 0)  by definition {operator*,operator*,operator*}
    suffices 0 < suc(pn') + suc(pn')  by replace add_zero[suc(pn')]
    suffices 0 < suc(pn' + suc(pn'))  by definition operator+
    suffices 0 < suc(suc(pn' + pn'))  by replace add_suc[pn'][pn']
    definition {operator<, operator≤, operator≤}
  }
end

/*
 Properties of Division and Modulo
 */

// Division by iterated subtraction.
recfun operator /(n : Nat, m : Nat) -> Nat
  measure n
{
  if n < m then 0
  else if m = 0 then 0
  else 1 + (n - m) / m
}
terminates {
	arbitrary n:Nat, m:Nat
  assume cond: not (n < m) and not (m = 0)
  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 sub_add_identity[n,m] to m_n
  }
  obtain m' where m_sm: 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 definition operator+ | operator< | operator≤
  suffices n ≤ n + m' by replace add_commute
  less_equal_add
}

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

lemma strong_induction_aux: all P: fn Nat -> bool.
  if (all n:Nat. if (all k:Nat. if k < n then P(k)) then P(n))
  then (all j:Nat, k:Nat. if k < j then P(k))
proof
  arbitrary P: fn Nat -> bool
  assume H
  induction Nat
  case 0 {
    arbitrary k:Nat
    assume neg_k
    conclude false by apply not_less_zero to neg_k
  }
  case suc(j') assume IH {
    arbitrary k:Nat
    assume: k < suc(j')
    have: k ≤ j' by evaluate in recall k < suc(j')
    cases (apply less_equal_implies_less_or_equal to recall k ≤ j')
    case: k < j' {
      conclude P(k) by apply IH to recall k < j'
    }
    case: k = j' {
      have A: all m:Nat. if m < j' then P(m) by {
        arbitrary m:Nat
        assume: m < j'
        have B: all k':Nat. (if k' < m then P(k')) by {
          arbitrary k':Nat
          assume: k' < m
          have: k' < j' by apply less_trans to (recall k' < m), (recall m < j')
          conclude P(k') by apply IH to recall k' < j'
        }
        conclude P(m) by apply H[m] to B
      }
      have: P(j') by apply H[j'] to A
      conclude P(k) by replace symmetric (recall k = j') in recall P(j')
    }
  }
end
  
theorem 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)
proof
  arbitrary P: fn Nat -> bool, n:Nat
  assume prem
  have X: all j:Nat, k:Nat. if k < j then P(k)
    by apply strong_induction_aux[P] to prem
  have: n < suc(n) by {
    suffices n ≤ n  by evaluate
    less_equal_refl
  }
  conclude P(n) by apply X[suc(n),n] to recall n < suc(n)
end

private fun DivPred(n:Nat) {
	all m:Nat. if 0 < m then some r:Nat. (n / m) * m + r = n and r < m
}

lemma division: all n:Nat, m:Nat.
  if 0 < m
  then some r:Nat. (n/m)*m + r = n and r < m
proof
  arbitrary n:Nat
  have SI: all j:Nat. if (all i:Nat. if i < j then DivPred(i)) then DivPred(j) by {
    arbitrary j:Nat
    assume prem: all i:Nat. if i < j then DivPred(i)
    suffices all m:Nat. if 0 < m then some r:Nat. ((j / m) * m + r = j and r < m)
      by definition DivPred
    arbitrary m:Nat
    assume m_pos
    switch j < m {
      case true assume j_m_true {
        suffices some r:Nat. r = j and r < m
          by definition operator / and replace j_m_true | zero_mult | zero_add
        choose j
        conclude j = j and j < m
          by replace j_m_true
      }
      case false assume j_m_false {
        switch m = 0 {
          case true assume m_z_true {
            have: m = 0 by replace m_z_true
            conclude false by apply less_irreflexive to replace (recall m = 0) in m_pos
          }
          case false assume m_z_false {
            have not_m_z: not (m = 0) by replace m_z_false
            have not_j_m: not (j < m) by replace j_m_false
            have m_j: m ≤ j by apply not_less_implies_less_equal to not_j_m
            obtain m' where m_sm: m = suc(m') from apply not_zero_suc to not_m_z
            suffices some r:Nat. ((1 + (j - m) / m) * m + r = j and r < m)
              by definition operator / and replace j_m_false | m_z_false
            suffices some r:Nat. (m + ((j - m) / m) * m + r = j and r < m)
              by replace dist_mult_add_right | one_mult
            have jm_j: j - m < j by {
              suffices m + (j - m) < m + j by add_both_sides_of_less[m,j-m,j]
              suffices j < m + j by replace apply sub_add_identity[j,m] to m_j
              suffices __ by replace m_sm
              suffices j ≤ m' + j by definition operator+ | operator< | operator≤
              suffices __ by replace add_commute
              less_equal_add
            }
            have div_mp: DivPred(j - m) by apply prem[j - m] to jm_j
            obtain r where div_jm: ((j - m) / m) * m + r = j - m and r < m
              from apply (definition DivPred in div_mp)[m] to m_pos
            choose r
            suffices (m + (j - m) = j and r < m) by replace conjunct 0 of div_jm
            have mjm_j: m + (j - m) = j by apply sub_add_identity[j, m] to m_j
            mjm_j, conjunct 1 of div_jm
          }
        }
      }
    }
  }
  have: DivPred(n) by apply strong_induction[DivPred, n] to SI
  definition DivPred in recall DivPred(n)
end

theorem div_mod: all n:Nat, m:Nat.
  if 0 < m
  then (n / m) * m + (n % m) = n
proof
  arbitrary n:Nat, m:Nat
  assume m_pos: 0 < m
  have p1: 0 * m ≤ n by evaluate
  have p2: n < (1 + (0 + (1 + n) * m)) * m by {
    obtain m' where m_sm: m = suc(m') from apply positive_suc to m_pos
    suffices __ by replace m_sm | zero_add | dist_mult_add_right[1,n] | mult_commute[n]
      | suc_one_add[m'] | dist_mult_add_right[1,m',n] | one_mult | dist_mult_add | mult_one
      | add_commute[m',n] | add_commute[1,n]
    suffices __ by definition operator< and replace suc_one_add[n]
    less_equal_add[1+n]
  }
  have ex: some r:Nat. (n/m)*m + r = n and r < m
    by apply division[n,m] to m_pos
  obtain r where R: (n/m)*m + r = n and r < m from ex
  suffices __ by definition operator%
  define a = (n / m) * m
  have ar_n: a + r = n by R
  have a_le_a_r: a ≤ a + r by less_equal_add
  have n_eq_a_r: n = a + r by symmetric (conjunct 0 of R)
  have a_le_n: a ≤ n by {
    suffices a ≤ a + r by replace n_eq_a_r
    a_le_a_r
  }
  conclude a + (n - a) = n
    by apply sub_add_identity to a_le_n
end

theorem mod_less_divisor: all n:Nat, m:Nat. if 0 < m then n % m < m
proof
  arbitrary n:Nat, m:Nat
  assume m_pos: 0 < m
  suffices __ by definition operator%
  obtain r where R: (n / m) * m + r = n and r < m
    from apply division[n, m] to m_pos
  define a = (n / m)*m
  have ar_n: a + r = n by R
  have ar_a_a: (a + r) - a = r  by add_sub_identity[a][r]
  have r_na: r = n - a by {
    suffices __ by replace symmetric ar_n
    symmetric ar_a_a
  }
  suffices r < m   by replace symmetric r_na
  conjunct 1 of R
end

lemma mult_div_mod_self: all y:Nat.
  if 0 < y
  then y / y = 1 and y % y = 0
proof
  arbitrary y:Nat
  assume y_pos: 0 < y
  have div_rem: (y / y) * y + (y % y) = y
    by apply div_mod[y,y] to y_pos
  have rem_less: y % y < y
    by apply mod_less_divisor[y, y] to y_pos
  switch (y / y) {
    case 0 assume yyz {
      have rem_eq: y % y = y by replace yyz | zero_mult | zero_add in div_rem
      conclude false by apply (apply less_not_equal to rem_less) to rem_eq
    }
    case suc(y') assume ysy {
      have eq1: y + (y' * y + y % y) = y + 0 by {
        suffices __ by replace add_zero
        definition operator* in replace ysy in div_rem
      }
      have eq2: y' * y + y%y = 0 by apply left_cancel to eq1
      have rem_zero: y % y = 0 by apply add_to_zero to eq2
      suffices suc(y') = 1 by replace rem_zero | ysy
      have yz: y' = 0 by {
        have yyz: y' * y = 0 by apply add_to_zero to eq2
        obtain y'' where ysy2: y = suc(y'') from apply positive_suc to y_pos
        have eq3: y' + y'' * y' = 0 by {
          definition operator* in
          replace ysy2 | mult_commute in yyz
        }
        conclude y' = 0 by apply add_to_zero to eq3
      }
      conclude suc(y') = 1 by replace yz
    }
  }
end

theorem div_cancel: all y:Nat. if 0 < y then y / y = 1
proof
  arbitrary y:Nat
  assume y_pos: 0 < y
  apply mult_div_mod_self[y] to y_pos
end

theorem mod_self_zero: all y:Nat. y % y = 0
proof
  arbitrary y:Nat
  switch y {
    case 0 {
      suffices __ by definition operator%
      zero_sub
    }
    case suc(y') assume y_sy {
      have y_pos: 0 < y by {
        suffices __ by replace y_sy
        evaluate
      }
      suffices y % y = 0 by replace symmetric y_sy
      apply mult_div_mod_self[y] to y_pos
    }
  }
end

theorem zero_mod: all x:Nat. 0 % x = 0
proof
  arbitrary x:Nat
  suffices __ by definition operator%
  zero_sub
end

theorem zero_div: all x:Nat. if 0 < x then 0 / x = 0
proof
  arbitrary x:Nat
  assume xpos
  have eq1: (0/x)*x + (0 % x) = 0 by apply div_mod[0,x] to xpos
  have eq2: (0/x)*x = 0  by apply add_to_zero to eq1
  switch x {
    case 0 assume xz {
      conclude false by apply (apply less_not_equal to xpos) to rewrite xz
    }
    case suc(x') assume xsx {
      have eq3: 0 / suc(x') + x' * (0 / suc(x')) = 0
        by definition operator* in rewrite xsx | mult_commute in eq2
      conclude 0 / suc(x') = 0 by apply add_to_zero to eq3
    }
  }
end

theorem mod_one: all n:Nat. n % 1 = 0
proof
  arbitrary n:Nat
  have one_pos: 0 < 1 by evaluate
  have n1_1:  n % 1 < 1 by apply mod_less_divisor[n,1] to one_pos
  switch n % 1 {
    case 0 assume n1z { n1z }
    case suc(n') assume n1_sn {
      conclude false by evaluate in replace n1_sn in n1_1
    }
  }
end

theorem div_one: all n:Nat. n / 1 = n
proof
  arbitrary n:Nat
  have one_pos: 0 < 1 by evaluate
  have eq1: (n / 1) * 1 + (n % 1) = n by apply div_mod[n,1] to one_pos
  have eq2: (n / 1) + (n % 1) = n by replace mult_one in eq1
  replace mod_one | add_zero in eq2
end

theorem add_div_one: all n:Nat, m:Nat.
  if 0 < m
  then (n + m) / m = 1 + n / m
proof
  arbitrary n:Nat, m:Nat
  assume m_pos
  have not_nm_m: not (n + m < m) by {
    assume nm_m: n + m < m
    have not_m_nm: not (m ≤ n + m) by apply not_less_equal_iff_greater to nm_m
    have: m ≤ m + n by less_equal_add
    have m_nm: m ≤ n + m by replace add_commute in recall m ≤ m + n
    conclude false by apply not_m_nm to m_nm
  }
  have m_nz: not (m = 0) by {
    assume: m = 0
    conclude false by evaluate in replace (recall m = 0) in m_pos
  }
    
  equations
      (n + m) / m = 1 + ((n + m) - m) / m  by definition operator/
                                             and replace (apply eq_false to not_nm_m)
                                                       | (apply eq_false to m_nz)
              ... = 1 + n / m              by replace add_commute[n,m]
                                                    | add_sub_identity
end
  
theorem mult_div_inverse: all n:Nat, m:Nat.
  if 0 < m then (n * m) / m = n
proof
  induction Nat
  case 0 {
    arbitrary m:Nat
    assume prem
    suffices 0 / m = 0 by replace zero_mult
    apply zero_div to prem
  }
  case suc(n') assume IH {
    arbitrary m:Nat
    assume prem
    suffices (n' * m + m) / m = suc(n')   by definition operator* and replace add_commute
    equations
        (n' * m + m) / m = 1 + (n' * m) / m  by apply add_div_one[n'*m, m] to prem
                     ... = 1 + n'            by replace apply IH to prem
                     ... = suc(n')           by evaluate
  }
end


/* 
  Properties of exponentiation
  https://rocq-prover.org/doc/v8.9/stdlib/Coq.Numbers.NatInt.NZPow.html
  and
  https://coq.kwarc.info/Coq.Numbers.NatInt.NZPow.html
  */

theorem expt_one : all n : Nat.
  n ^ 1 = n
proof
  arbitrary n : Nat
  suffices n * 1 = n by evaluate
  mult_one
end

theorem one_expt : all n : Nat.
  1 ^ n = 1
proof
  induction Nat
  case 0 {
    evaluate
  }
  case suc(n') assume IH {
    have IH' : expt(n', 1) = 1 by definition operator^ in IH
    suffices 1 * expt(n', 1) = 1 by definition operator^ | expt
    rewrite IH' | one_mult
  }
end

theorem pow_add_r : all n : Nat, m : Nat, o : Nat.
  m ^ (n + o) = m ^ n * m ^ o
proof
  induction Nat
  case zero {
    arbitrary m : Nat, o : Nat
    suffices expt(o, m) = expt(o, m) + 0 by evaluate
    replace add_zero
  }
  case suc(n') assume IH {
    arbitrary m : Nat, o : Nat
    have IH' : (all m':Nat, o':Nat. expt(n' + o', m') = expt(n', m') * expt(o', m')) 
      by definition operator^ in IH
    suffices  m * expt(n' + o, m) = m * expt(n', m) * expt(o, m) 
      by definition operator^ | operator+ | expt
    replace IH'
  }
end

theorem pow_mul_l : all o : Nat, m : Nat, n : Nat.
  (m * n) ^ o = m ^ o * n ^ o
proof
  induction Nat
  case 0 {
    evaluate
  }
  case suc(o') assume IH {
    arbitrary m : Nat, n : Nat
    have IH' : (all m':Nat, n':Nat. expt(o', m' * n') = expt(o', m') * expt(o', n')) 
      by evaluate in IH
    suffices  m * n * expt(o', m * n) = m * expt(o', m) * n * expt(o', n) by evaluate
    rewrite IH' | mult_commute[n, expt(o', m)]
  }
end

theorem pow_mul_r : all o : Nat, m : Nat, n : Nat.
  (m ^ n) ^ o = m ^ (n * o)
proof
  induction Nat
  case 0 {
    arbitrary m : Nat, n : Nat
    suffices (m ^ n) ^ 0 = m ^ 0 by replace mult_zero
    evaluate
  }
  case suc(o') assume IH {
    arbitrary m : Nat, n : Nat
    have IH' :  (all m':Nat, n':Nat. expt(o', expt(n', m')) = expt(n' * o', m')) 
      by definition operator^ in IH
    suffices expt(n, m) * expt(n * o', m) = expt(n + n * o', m)
      by definition operator^ | expt
      and rewrite mult_suc[n, o'] | IH'
    symmetric definition operator^ in pow_add_r[n, m, n * o']
  }
end

theorem pow_pos_nonneg : all b : Nat, a : Nat.
  if 0<a then 0<a^b
proof
  induction Nat
  case 0 {
    evaluate
  }
  case suc(b') assume IH {
    arbitrary a : Nat
    assume prem
    suffices 0 < a * expt(b', a) by definition operator^ | expt
    have exp_nz : 0 < expt(b', a) by definition operator^ in apply IH to prem
    apply mult_pos_nonneg to prem, exp_nz
  }
end


theorem pow_0_l : all a : Nat. if 0<a then 0^a = 0
proof
  arbitrary a : Nat
  switch a {
    case 0 {
      evaluate
    }
    case suc(n') {
      evaluate
    }
  }
end


theorem pow_eq_0 : all n : Nat, m : Nat.
  if m ^ n = 0 then m = 0
proof
  induction Nat
  case 0 {
    evaluate
  }
  case suc(n') assume IH {
    arbitrary m : Nat
    switch m {
      case 0 assume eq_z_t {
        evaluate
      }
      case suc(m') assume eq_sn_t {
        assume contra
        have contra' : suc(m') * expt(n', suc(m')) = 0 
          by definition operator^ | expt in contra
        have e_n_sm_z : expt(n', suc(m')) = 0 by apply mult_to_zero to contra'
        have IH' : all m'':Nat. if expt(n', m'') = 0 then m'' = 0 
          by definition operator^ in IH
        conclude false by apply IH'[suc(m')] to e_n_sm_z
      }
    }
  }
end

theorem exp_one_implies_zero_or_one : all m : Nat, n : Nat.
  if m ^ n = 1 then n = 0 or m = 1
proof 
  arbitrary m : Nat, n : Nat
  switch n {
    case 0  {
      .
    }
    case suc(n') {
      suffices  (if m * expt(n', m) = 1 then m = 1) by evaluate
      assume prem
      apply one_mult_one to prem
    }
  }
end

theorem pow_lt_mono_l : all  c : Nat, a : Nat, b : Nat.
  if 0 < c then if a < b then a ^ c < b ^ c
proof
  induction Nat
  case 0 {
    evaluate
  }
  case suc(n') assume IH {
    arbitrary a : Nat, b : Nat
    assume z_l_sc
    assume alb
    switch 0 < n' {
      case true assume prop_t {
        suffices a * expt(n', a) < b * expt(n', b) 
          by definition operator^ | expt
        have ena_l_enb : expt(n', a) < expt(n', b) 
          by definition operator^ in apply (rewrite prop_t in IH) to alb
        have enb_nz :  expt(n', b) > 0
          by suffices __ by definition operator >
         apply greater_any_zero to ena_l_enb
        have bnz : 0 < b 
          by apply greater_any_zero to alb
        have step1 : a * expt(n', a) <= a * expt(n', b)
          by apply mult_mono_le[a, expt(n', a), expt(n', b)] to 
            (apply less_implies_less_equal to ena_l_enb)
        have step2 : a * (expt(n',b)) < b * expt(n', b) 
          by apply (apply mult_lt_mono_l[expt(n', b), a, b] to enb_nz) to alb

        cases (apply less_equal_implies_less_or_equal to step1) 
        case step1':  a * expt(n', a) < a * expt(n', b) {
          apply less_trans[a * expt(n', a), a * expt(n', b)] to step1', step2
        }
        case step1'':  a * expt(n', a) = a * expt(n', b) {
          replace symmetric step1'' in step2
        }
      }
      case false assume prop_f {
        have nz : n' = 0 by rewrite prop_f in zero_or_positive[n']
        suffices a < b by rewrite nz | expt_one
        alb
      }
    }
  }
end

theorem pow_gt_1 : all n : Nat, m : Nat.
  if 1 < n then (0 < m <=> 1 < n ^ m)
proof
  arbitrary n : Nat, m : Nat
  assume prem
  have l : if 0 < m then 1 < n ^ m
    by assume zlm
       suffices 1^m < n^m by rewrite symmetric one_expt[m]
       suffices 1 < n by apply pow_lt_mono_l[m, 1, n] to zlm
       prem
  have r : if 1 < n ^ m then 0 < m
    by assume nm_g1
       cases zero_or_positive[m]
       case zm : m = 0 {
        evaluate in rewrite zm in nm_g1 
       }
       case : 0 < m { recall 0 < m }
  r, l
end

theorem pow_le_mono_l : all c : Nat, a : Nat, b : Nat.
  if a <= b then a ^ c <= b ^ c
proof 
  induction Nat
  case 0 {
    evaluate
  }
  case suc(n') assume IH {
    arbitrary a : Nat, b : Nat
    assume a_le_b
    suffices  a * expt(n', a) ≤ b * expt(n', b) 
      by definition operator^ | expt
    have step : expt(n', a) <= expt(n', b)
      by definition operator^ in (apply IH to a_le_b)
    have step1 : a * expt(n', a) <= a * expt(n', b)
      by apply mult_mono_le[a, expt(n', a), expt(n', b)] to step
    have step2 : a * expt(n', b) <= b * expt(n', b)
      by apply mult_mono_le_r[expt(n', b), a, b] to a_le_b
    apply less_equal_trans[a * expt(n', a), a * expt(n', b)] to step1, step2
  }
end

theorem pow_lt_mono_r : all c : Nat, a : Nat, b : Nat.
  if 1 < a then if b < c then a^b < a^c
proof
  arbitrary c : Nat, a : Nat, b : Nat
  assume prem
  assume blc
  have blec : b <= c by apply less_implies_less_equal to blc
  obtain x where step from apply le_exists_sub to blec
  suffices a ^ b < a ^ b * a ^ x 
    by rewrite step | pow_add_r
  suffices 1 * a ^ b < a ^ x * 1 * a ^ b
    by rewrite mult_commute[a^b, a^x] | symmetric one_mult[a^b]
  have zla : 0 < a by 
    have zl1 : 0 < 1 by evaluate
    apply less_trans[0, 1, a] to zl1, prem
  have : a ^ b > 0 by
    suffices __ by definition operator>
    apply pow_pos_nonneg[b, a] to  zla
  suffices 1 < a^x * 1
    by (apply mult_lt_mono_l[a^b, 1, a^x * 1] to recall a^b > 0)
  have zlx : 0 < x 
    by cases zero_or_positive[x]
    case xz : x = 0 {
      have cb : c = b by rewrite xz | add_zero in step
      apply less_irreflexive to rewrite cb in blc 
    }
    case : 0 < x { recall 0 < x }
  rewrite symmetric mult_one[a^x] in apply (apply pow_gt_1[a, x] to prem) to zlx
end

theorem pow_inj_l : all a : Nat, b : Nat, c : Nat.
  if 0 < c then (if a^c = b^c then a = b)
proof
  arbitrary a : Nat, b : Nat, c : Nat
  assume zlc
  assume ac_eq_bc
  cases trichotomy[a, b]
  case : a < b {
    have contra : a^c < b^c by apply (apply pow_lt_mono_l[c, a, b] to zlc) to (recall a < b)
    apply less_irreflexive to rewrite ac_eq_bc in contra
  }
  case : a = b { recall a = b }
  case : b < a {
    have contra : b^c < a^c by apply (apply pow_lt_mono_l[c, b, a] to zlc) to (recall b < a)
    apply less_irreflexive to rewrite ac_eq_bc in contra
  }
end

theorem pow_inj_r : all a : Nat, b : Nat, c : Nat.
  if 1 < a then if a^b = a ^ c then b = c
proof
  arbitrary a : Nat, b : Nat, c : Nat
  assume ola
  assume ab_eq_ac
  cases trichotomy[b, c]
  case : b < c {
    apply less_irreflexive to
      rewrite ab_eq_ac in
      apply apply pow_lt_mono_r[c,a,b] to ola to recall b < c
  }
  case : b = c { recall b = c }
  case : c < b {
    apply less_irreflexive to
      rewrite ab_eq_ac in
      apply apply pow_lt_mono_r[b,a,c] to ola to recall c < b
  }
end