Nat.pf

import Option

union Nat {
  zero
  suc(Nat)
}

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

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

function 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')) }
    }
}

function pred(Nat) -> Nat {
  pred(0) = 0
  pred(suc(n)) = n
}

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

union Pos {
  one
  succ(Pos)
}

function nat2pos(Nat) -> Option<Pos> {
  nat2pos(0) = none
  nat2pos(suc(n')) =
    switch nat2pos(n') {
      case none {
        just(one)
      }
      case just(p) {
        just(succ(p))
      }
    }
}

function pos2nat(Pos) -> Nat {
  pos2nat(one) = 1
  pos2nat(succ(p)) = suc(pos2nat(p))
}

function find_quotient(Nat,Nat,Pos,Nat) -> Nat {
  find_quotient(0, n, m, q) = q
  find_quotient(suc(u), n, m, q) =
    if suc(q) * pos2nat(m) ≤ n then
      (if n < u * pos2nat(m) then
         find_quotient(u, n, m, suc(q))
       else
         u)
    else
      q
}

function operator /(Nat,Pos) -> Nat {
  operator /(0, m) = 0
  operator /(suc(n'), m) =
    find_quotient(suc(suc(n')) * pos2nat(m), suc(n'), m, 0)
}

function operator%(Nat,Pos) -> Nat {
  operator %(0, m) = 0
  operator %(suc(n'), m) = suc(n') - (suc(n') / m) * pos2nat(m)
}

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

define operator < : fn Nat,Nat -> bool = λ x, y { suc(x) ≤ y }
define operator > : fn Nat,Nat -> bool = λ x, y { y < x }
define operator ≥ : fn Nat,Nat -> bool = λ x, y { y ≤ x }

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

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

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

function div2(Nat) -> Nat {
  div2(0) = 0
  div2(suc(n')) = div2_aux(n')
}

function div2_aux(Nat) -> Nat {
  div2_aux(0) = 0
  div2_aux(suc(n')) = suc(div2(n'))
}

function 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') }
    }
}

function 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 rewrite IH
  }
end

lemma 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

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

lemma add_suc: all m:Nat. all n:Nat.
  m + suc(n) = suc(m + n)
proof
  enable operator +
  induction Nat
  case 0 {
    arbitrary n : Nat
    conclude 0 + suc(n) = suc(0 + n)  by .
  }
  case suc(n') suppose IH {
    arbitrary n : Nat
    equations
      suc(n') + suc(n) = suc(n' + suc(n))  by .
                   ... = suc(suc(n' + n))  by rewrite IH[n]
                   ... = suc(suc(n') + n)  by .
  }
end

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

theorem one_add: all m:Nat.  1 + m = suc(m)
proof
  arbitrary m:Nat
  definition {operator+, 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. all n:Nat, o:Nat.
  (m + n) + o = m + (n + o)
proof
  enable operator +
  induction Nat
  case 0 {
    arbitrary n:Nat, o:Nat
    conclude (0 + n) + o = 0 + (n + o)   by .
  }
  case suc(m') suppose IH {
    arbitrary n:Nat, o:Nat
    equations
      (suc(m') + n) + o = suc((m' + n) + o)  by .
                    ... = suc(m' + (n + o))  by rewrite IH[n,o]
                    ... = suc(m') + (n + o)  by .
  }
end

theorem left_cancel: all x:Nat. all y:Nat, z:Nat.
  if x + y = x + z then y = z
proof
  enable operator +
  induction Nat
  case 0 {
    arbitrary y:Nat, z:Nat
    suppose prem: 0 + y = 0 + z
    equations   y = 0 + y      by .
              ... = 0 + z      by prem
              ... = z          by .
  }
  case suc(x') suppose IH {
    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 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 mz: m = 0
      by definition operator + in zmz
    rewrite mz
  }
  case suc(n') suppose IH {
    arbitrary m:Nat
    suppose snmz: suc(n') + m = 0
    conclude false
        by definition operator + in snmz
  }
end

/*
 Properties of pred
 */
 
theorem pred_one: pred(suc(0)) = 0
proof
  definition pred
end

/*
 Properties of Subtraction
 */
 
theorem sub_cancel: all n:Nat. n - n = 0
proof
  induction Nat
  case 0 {
    conclude 0 - 0 = 0   by definition operator-
  }
  case suc(n') suppose 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 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 rewrite zero_add[n]
                        ... = 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 rewrite suc_add[m',n]
          ... = (m' + n) - m'              by definition operator-
          ... = n                          by IH[n]
  }
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

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

lemma 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 {
    arbitrary n:Nat
    suffices suc(n + m' * suc(n)) = suc(m' + (n + m' * n))
        with definition {operator*, operator+}
    equations   suc(n + m' * suc(n))
              = suc(n + (m' + m' * n))       by rewrite IH[n]
          ... ={ suc((n + m') + m' * n) }    by rewrite add_assoc[n][m', m' * n]
          ... = suc((m' + n) + m' * n)       by rewrite add_commute[n][m']
          ... = suc(m' + (n + m' * n))       by rewrite add_assoc[m'][n, m' * n]
  }
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 rewrite IH[n]
           ... = 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 rewrite zero_mult[n]
                  ... = 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 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 rewrite one_mult[n]
end

theorem dist_mult_add:
  all a:Nat. all 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 rewrite zero_mult[x] | zero_mult[y]
  }
  case suc(a') suppose IH {
    arbitrary x:Nat, y:Nat
    suffices (x + y) + a' * (x + y) = (x + a' * x) + (y + a' * y)
        with definition operator *
    equations
            (x + y) + a' * (x + y)
          = (x + y) + (a' * x + a' * y)       by rewrite IH[x,y]
      ... = ((x + y) + a' * x) + a' * y       by symmetric add_assoc[x+y][a'*x,a'*y]
      ... = (x + (y + a' * x)) + a' * y       by rewrite add_assoc[x][y,a'*x]
      ... = (x + (a' * x + y)) + a' * y       by rewrite add_commute[y][a'*x]
      ... = ((x + a' * x) + y) + a' * y       by rewrite symmetric add_assoc[x][a'*x,y]
      ... = (x + a' * x) + (y + a' * y)       by add_assoc[x+a'*x][y,a'*y]
  }
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 mult_commute[x+y][a]
          ... = a * x + a * y       by dist_mult_add[a][x,y]
          ... = x * a + a * y       by rewrite mult_commute[a][x]
          ... = x * a + y * a       by rewrite mult_commute[a][y]
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 rewrite zero_mult[n]
                        ... = 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 rewrite IH[n,o]
    ... = {suc(m') * (n * o)}   by definition operator*
  }
end

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

theorem suc_less_equal: all x:Nat, y:Nat.
  if suc(x) ≤ suc(y)
  then x ≤ y
proof
  arbitrary x:Nat, y:Nat
  suppose prem
  definition operator≤ in prem
end

theorem suc_less_equal_suc: all x:Nat, y:Nat.
  if x ≤ y
  then suc(x) ≤ suc(y)
proof
  arbitrary x:Nat, y:Nat
  suppose prem
  suffices x ≤ y   with definition operator ≤
  prem
end

theorem less_suc: all x:Nat, y:Nat.
  if x < y
  then suc(x) < suc(y)
proof
  arbitrary x:Nat, y:Nat
  suppose x_l_y: x < y
  suffices suc(suc(x)) ≤ suc(y)   with definition operator<
  suffices suc(x) ≤ y             with definition operator≤ 
  definition operator< in x_l_y
end

theorem suc_less: all x:Nat, y:Nat.
  if suc(x) < suc(y)
  then x < y
proof
  arbitrary x:Nat, y:Nat
  suppose prem
  suffices suc(x) ≤ y      with definition operator<
  apply suc_less_equal[suc(x), y] to definition operator< in prem
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')    with definition operator<
        suffices 0 ≤ y'              with 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 rewrite yz in sx_le_y
      }
      case suc(y') suppose y_sy {
        have x_le_y: x' ≤ y'
          by definition operator≤ in rewrite y_sy in sx_le_y
        have xy_or_xy: x' < y' or x' = y'
          by apply IH[y'] to x_le_y
        cases xy_or_xy
        case x_l_y {
          have sx_l_sy: suc(x') < suc(y')
            by apply less_suc 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 rewrite x_y
          conclude (suc(x') < suc(y') or suc(x') = suc(y'))
            by sx_sy
        }
      }
    }
  }
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 (rewrite yz in ssx_y)
      }
      case suc(y') suppose EQ : y = suc(y') {
        have ssx_sy: suc(suc(x')) ≤ suc(y')  by rewrite EQ in ssx_y
        have x_y: x' < y'
            by suffices suc(x') ≤ y'  with definition operator <
               definition operator ≤ in ssx_sy
        suffices suc(x') ≤ suc(y')   by .
        suffices x' ≤ y'   with definition operator ≤          
        apply IH[y'] to x_y
      }
    }
  }
end

theorem less_equal_refl: all n:Nat. n ≤ n
proof
  enable operator ≤
  induction Nat
  case 0 { conclude 0 ≤ 0  by . }
  case suc(n') suppose IH { conclude suc(n') ≤ suc(n')  by 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  with rewrite 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 rewrite 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 sx_z: suc(x') ≤ 0 by rewrite y_z in sxy_ysx
        conclude false by definition operator ≤ in sx_z
      }
      case suc(y') suppose y_suc {
        enable operator ≤
        have x_le_y: x' ≤ y' by rewrite y_suc in sxy_ysx
        have y_le_x: y' ≤ x' by rewrite y_suc in sxy_ysx
        have x_y: x' = y' by (apply IH[y'] to x_le_y, y_le_x)
        conclude suc(x') = suc(y') by rewrite 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
  enable operator ≤
  induction Nat
  case 0 {
    arbitrary n:Nat, o:Nat
    suppose _
    conclude 0 ≤ o  by .
  }
  case suc(m') suppose IH {
    arbitrary n:Nat, o:Nat
    suppose Prem: suc(m') ≤ n and n ≤ o
    have sm_n: suc(m') ≤ n  by Prem // bug
    have n_o: n ≤ o  by Prem
    switch n {
      case 0 suppose nz {
        have sm_z: suc(m') ≤ 0  by rewrite nz in sm_n
        conclude false  by sm_z
      }
      case suc(n') suppose ns {
        have sm_sn: suc(m') ≤ suc(n')  by rewrite ns in sm_n
        have m_n: m' ≤ n'  by sm_sn
        have sn_o: suc(n') ≤ o  by rewrite ns in n_o
        switch o {
          case 0 suppose oz {
            have sn_z: suc(n') ≤ 0  by rewrite oz in sn_o
            conclude false  by sn_z
          }
          case suc(o') suppose os {
            have sn_so: suc(n') ≤ suc(o')  by rewrite os in sn_o
            have n_o: n' ≤ o'  by sn_so
            conclude m' ≤ o'  by apply IH[n',o'] to m_n, n_o
          }
        }
      }
    }
  }
end

theorem not_less_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 (rewrite ys in not_0_y)
                          to (suffices 1 ≤ suc(y')   with 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')  with definition operator <
                 suffices suc(x') ≤ y'            with definition operator ≤
                 (definition operator < in x_y)
            have sx_y: suc(x') < y by (suffices suc(x') < suc(y')  with rewrite ys
                                       sx_sy)
            apply not_sx_y to sx_y)
        suffices y' ≤ x'  with 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
    enable {operator <, operator ≤}
    conclude false by 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 suc_less to sx_l_sx
    conclude false by apply IH to x_l_x
  }
end

theorem less_not_greater_equal:
  all x:Nat. all y:Nat.
  if x < y then not (y ≤ x)
proof
  induction Nat
  case zero {
    arbitrary y : Nat
    suppose z_l_y: 0 < y
    suppose y_le_z: y ≤ 0
    switch y {
      case zero suppose y_z: y = 0 {
        definition {operator <, operator ≤}
        in (rewrite y_z in z_l_y)
      }
      case suc(y') suppose y_s: y = suc(y') {
        definition {operator ≤}
        in (rewrite y_s in y_le_z)
      }
    }
  }
  case suc(x') suppose IH {
    arbitrary y : Nat
    suppose sx_less_y
    suppose y_le_sx
    switch y {
      case zero suppose y_eq_zero {
        enable {operator <, operator ≤}
        conclude false  by rewrite y_eq_zero in sx_less_y
      }
      case suc(y') suppose ys {
        enable {operator <, operator ≤}
        have x_less_y: x' < y' by  rewrite ys in sx_less_y
        have y_le_x: y' ≤ x' by  rewrite ys in y_le_sx
        conclude false  by apply (apply IH[y'] to x_less_y) to y_le_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_l_y: x < y
  suppose x_y: x = y
  have y_l_y: y < y by rewrite x_y in x_l_y
  conclude false by apply less_irreflexive[y] to y_l_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_g_y: x > y
  suppose x_y: x = y
  have y_g_y: y > y  by rewrite x_y in x_g_y
  have y_l_y: y < y  by definition operator> in y_g_y
  conclude false by apply less_irreflexive[y] to y_l_y
end

theorem less_implies_not_less_equal:
  all x:Nat. all y:Nat.
  if x < y then not (y ≤ x)
proof
  induction Nat
  case zero {
    arbitrary y:Nat
    suppose y_pos
    suppose y_le_z
    switch y {
      case 0 suppose y_z {
        conclude false   by definition {operator <, operator≤} in
                            rewrite y_z in y_pos
      }
      case suc(y') suppose y_sy {
        conclude false   by definition operator≤ in rewrite y_sy in y_le_z
      }
    }
  }
  case suc(x') suppose IH {
    arbitrary y:Nat
    suppose sx_l_y
    suppose y_le_sx
    switch y {
      case 0 suppose y_z {
        conclude false  by definition{operator<, operator≤} in
                           rewrite y_z in sx_l_y
      }
      case suc(y') suppose y_sy {
        have x_l_y: x' < y'
          by suffices suc(x') ≤ y' with definition operator<
             definition {operator ≤} in
             definition {operator<} in rewrite y_sy in sx_l_y
        have y_le_x: y' ≤ x'
          by definition operator≤ in rewrite y_sy in y_le_sx
        conclude false  by apply (apply IH[y'] to x_l_y) to y_le_x
      }
    }
  }
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
    suppose y_less_sx
    switch y {
      case zero suppose y_eq_zero {
        conclude false by (definition {operator <, operator ≤} in
                       (rewrite y_eq_zero in sx_less_y))
      }
      case suc(y') suppose ys {
        enable {operator<,operator≤}
        have x_less_y: x' < y'  by rewrite ys in sx_less_y
        have y_less_x: y' < x'  by rewrite ys in y_less_sx
        conclude false by apply (apply IH[y'] to x_less_y) to y_less_x
      }
    }
  }
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') {
        enable {operator <, operator ≤, operator ≤}
        conclude 0 < suc(y') by .
      }
    }
  }
  case suc(x') suppose IH {
    arbitrary y:Nat
    switch y {
      case zero {
        conclude 0 < suc(x')
          by definition {operator<, operator≤, 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')  with definition operator <
               suffices suc(x') ≤ y'            with definition operator ≤ 
               definition operator < in less
        }
        case equal { conclude suc(x') = suc(y')  by rewrite equal }
        case greater {
          conclude suc(y') < suc(x')
              by suffices suc(suc(y')) ≤ suc(x')   with definition operator <
                 suffices suc(y') ≤ x'             with 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 equal: x = y {
    have not_equal: not (x = y)  by prem
    conclude false  by apply not_equal to equal
  }
  case greater: y < x {
    conclude y <  x by greater
  }
end

theorem 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

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

theorem less_implies_less_equal:
  all x:Nat. all y:Nat.
  if x < y  then  x ≤ y
proof
  //enable {operator ≤, operator <}
  induction Nat
  case zero {
    arbitrary y:Nat
    suppose z_y: 0 < y
    conclude 0 ≤ y by definition operator ≤
  }
  case suc(x') suppose IH {
    arbitrary y:Nat
    switch y {
      case zero {
        definition {operator <, operator ≤}
      }
      case suc(y') {
        suppose sx_sy: suc(x') < suc(y')
        enable {operator ≤, operator ≤, operator <}
        have x_y: x' < y' by sx_sy
        have x_le_y: x' ≤ y' by (apply IH[y'] to x_y)
        conclude suc(x') ≤ suc(y') by x_le_y
      }
    }
  }
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  with rewrite 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 <, operator ≤, 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_greater:
  all x:Nat, y:Nat.
  if not (x ≤ y) then y < x
proof
  arbitrary x:Nat, y:Nat
  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
  }
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_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   with 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
     with rewrite add_commute[x][y]
  less_equal_add[y][x]
end

theorem less_equal_suc: all n:Nat.
  n ≤ suc(n)
proof
  arbitrary n:Nat
  definition {operator+,operator+} in
  rewrite add_commute[n][1] in
  less_equal_add[n][1]
end

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   with 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 with 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 less_one_add: all n:Nat.
  0 < 1 + n
proof
  arbitrary n:Nat
  definition {operator<, operator≤, operator+, operator≤}
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  with definition operator<
  have sx_le_y: 1 + x ≤ y  by
    suffices suc(x) ≤ y  with definition {operator+,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

theorem less_equal_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 y_le_z: 0 + y ≤ 0 + z
    conclude y ≤ z
        by definition {operator+} in y_le_z
  }
  case suc(x') suppose IH {
    arbitrary y:Nat, z:Nat
    suppose sx_y_le_sx_z: suc(x') + y ≤ suc(x') + z
    have x_y_le_x_z: x' + y ≤ x' + z
      by definition {operator +, operator ≤} in sx_y_le_sx_z
    conclude y ≤ z
      by apply IH[y,z] to x_y_le_x_z
  }
end

theorem less_left_cancel: all x:Nat, y:Nat, z:Nat.
  if x + y < x + z then y < z
proof
  arbitrary x:Nat, y:Nat, z:Nat
  suffices if suc(x + y) ≤ x + z then suc(y) ≤ z   with definition operator <
  suppose sxy_xz: suc(x + y) ≤ x + z
  have x_sy_le_xz: x + suc(y) ≤ x + z
    by suffices suc(x + y) ≤ x + z  with rewrite add_suc[x][y]
       sxy_xz
  conclude suc(y) ≤ z
    by apply less_equal_left_cancel[x][suc(y), z] to x_sy_le_xz
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 rewrite add_zero[l]
    have m_z: m = 0 by apply zero_le_zero to m_le_z
    rewrite 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-}
        rewrite sub_zero[l + suc(n')]
      }
      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 rewrite add_suc[l][n']
        suffices l + (n' - m') = (l + n') - m'
             by definition operator-
        have m_n: m' ≤ n'
          by definition operator ≤ in rewrite m_sm in m_le_sn
        apply IH[l, m'] to m_n
      }
    }
  }
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 rewrite 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 {
        suffices 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 rewrite m_sm in m_le_sn
        have IH_m: m' + (n' - m') = n' by apply IH[m'] to m_n
        rewrite IH_m
      }
    }
  }
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 rewrite 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 rewrite n_sn
             in conjunct 0 of prem
        have m_no: m' ≤ n' + o
          by definition {operator ≤, operator +} in rewrite n_sn in 
             conjunct 1 of prem
        conclude m' - n' ≤ o  by apply IH[n',o] to n_m, m_no
      }
    }
  }
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')
      with definition max
    conclude suc(max(x', x')) = suc(x') by rewrite 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 rewrite 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 {
      suffices max(1,suc(y)) = suc(max(0,y)) by .
      definition {max, max}
    }
    case suc(x') {
      switch y {
        case 0 {
          definition {max, max}
        }
        case suc(y') {
          definition {max, max}
        }
      }
    }
  }
end

theorem max_greater_right: all y:Nat. all 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 rewrite max_suc2[x',y']
        suffices y' ≤ max(x',y')  by definition operator ≤
        IH[x']
      }
    }
  }
end

theorem max_greater_left: all x:Nat. all 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. all y:Nat.
  max(x, y) = x or max(x, y) = y
proof
  induction Nat
  case 0 {
    arbitrary y: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')   with definition max
          rewrite m_x
        }
        case m_y: max(x',y') = y' {
          suffices suc(max(x',y')) = suc(y')   with definition max
          rewrite 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. all y:Nat.
  max(x,y) = max(y,x)
proof
  induction Nat
  case 0 {
    arbitrary y:Nat
    suffices y = max(y, 0)  with definition max
    rewrite max_zero[y]
  }
  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'))
            with rewrite max_suc2[x',y'] | max_suc2[y',x']
        rewrite IH[y']
      }
    }
  }
end

theorem max_assoc: all x:Nat. all 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')))
               with definition max
            rewrite IH[y',z']
          }
        }
      }
    }
  }
end

theorem max_equal_greater_right: all x:Nat. all 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
                           rewrite y_z in sx_le_y
      }
      case suc(y') suppose y_suc {
        have x_l_y: x' ≤ y'
            by definition operator≤ in rewrite y_suc in sx_le_y
        conclude suc(max(x', y')) = suc(y')
            by rewrite apply IH to x_l_y
      }
    }
  }
end

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

theorem max_less_equal: all x:Nat. all 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  with 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
                   rewrite z_zero in prem
          }
          case suc(z') suppose z_suc {
            suffices max(x', y') ≤ z'  with definition operator≤
            have x_le_z: x' ≤ z' by
                definition operator≤ in rewrite z_suc in prem
            have y_le_z: y' ≤ z' by
                definition operator≤ in
                rewrite y_suc | z_suc in prem
            apply IH to x_le_z, y_le_z
          }
        }
      }
    }
  }
end


/*
 Odd and Even Numbers
 */

function is_even(Nat) -> bool {
  is_even(0) = true
  is_even(suc(n)) = is_odd(n)
}

function is_odd(Nat) -> bool {
  is_odd(0) = false
  is_odd(suc(n)) = is_even(n)
}

define Even : fn Nat -> bool = λ n { some m:Nat. n = 2 * m }
define Odd : fn Nat -> bool = λ n { some m:Nat. n = suc (2 * m) }

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
  suffices 2 * a + 2 * b = 2 * (a + b)  by rewrite x_2a | y_2b
  symmetric dist_mult_add[2][a,b]
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
            definition {operator *, operator *, operator *, operator +}
   have part2: if is_odd(0) then Odd(0)
     by suppose zero_odd
        conclude false by definition is_odd 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 definition is_even 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 rewrite n_2m
       suffices suc(suc(m + (m + 0))) = suc(m + suc(m + 0))
           by definition {operator *, operator *, operator *, operator+}
       rewrite add_zero[m] | add_suc[m][m])
    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 definition is_odd 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
       rewrite n_2m)
    part1, part2
  }
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
       rewrite add_zero[s] | add_zero[t] in
       (apply f_g[0] to definition {operator <, operator ≤, 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 .
            have fsi_gtsi: f(s + suc(i)) = g(t + suc(i))
              by apply f_g[suc(i)] to
                 enable {operator <, operator ≤, operator ≤} i_k
            enable operator + rewrite add_suc[s][i] | add_suc[t][i] in fsi_gtsi
    rewrite 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 (enable {operator <,operator ≤}
                                        suffices s ≤ s + k'
                                            by rewrite add_suc[s][k']
                                        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 apply IH[f,g,suc(s)] to (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
                                                 enable {operator <, operator +}
                                                 suffices suc(i) ≤ suc(s + k')  by rewrite add_suc[s][k']
                                                 (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)
    rewrite 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))  with 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 rewrite add_zero[s] | add_zero[t] 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 +
         rewrite add_suc[s][i] | add_suc[t][i] in f_g[suc(i)]
    equations
          f(s) + summation(k',suc(s),f)
        = g(t) + summation(k',suc(s),f)   by rewrite fs_gt
    ... = g(t) + summation(k',suc(t),g)   by rewrite (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
    enable {operator +}
    suffices summation(b,s,f) = summation(b,t,h)  by definition 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 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
        rewrite add_zero[s]
        in apply (conjunct 0 of g_f_and_h_f)[0]
           to definition {operator <, operator ≤, 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'
              enable {operator +, operator ≤}  rewrite add_suc[s][i] in
              (apply (conjunct 0 of g_f_and_h_f)[suc(i)] to enable {operator <, operator ≤} i_a)
         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
              enable {operator +} rewrite add_suc[s][a'+i] 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
    rewrite fs_gs | IH' | add_assoc[g(s)][summation(a',suc(s),g), summation(b,t,h)]
  }
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: all m:Nat. all n:Nat.
  if (m = n) then equal(m, n)
proof
  induction Nat
  case 0 {
    arbitrary n:Nat
    switch n {
      case 0 { definition equal }
      case suc(n') { . }
    }
  }
  case suc(m') {
    arbitrary n:Nat
    switch n {
      case 0 { . }
      case suc(n') {
        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 rewrite m_n
        equal_refl[n']
      }
    }
  }
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 rewrite m_n
                              equal_refl[n]
  apply not_m_n to eq_m_n
end

theorem equal_sound: all m:Nat. all n:Nat.
  if equal(m, n) then (m = n)
proof
  induction Nat
  case 0 {
    arbitrary n:Nat
    suppose eq
    switch n {
      case 0 { . }
      case suc(n') suppose n_sn {
        conclude false by definition equal in (rewrite n_sn in eq)
      }
    }
  }
  case suc(m') suppose IH {
    arbitrary n:Nat
    suppose eq: equal(suc(m'),n)
    switch n {
      case 0 suppose n_0 {
        conclude false by definition equal in rewrite n_0 in eq
      }
      case suc(n') suppose n_sn {
        have eq_mn: equal(m', n')
            by definition equal in rewrite n_sn in eq
        have m_n: m' = n'
            by apply IH[n'] to eq_mn
        conclude suc(m') = suc(n')
            by rewrite m_n
      }
    }
  }
end

/*
 Properties of div2
 */
 
theorem div2_add_2: all n:Nat.  div2(suc(suc(n))) = suc(div2(n))
proof
  arbitrary n:Nat
  definition {div2, div2_aux}
end

theorem div2_double: all n:Nat.
  div2(n + n) = n
proof
  induction Nat
  case 0 {
    definition {operator+, div2}
  }
  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 rewrite add_suc[n'][n']
    suffices suc(div2(n' + n')) = suc(n')       by rewrite div2_add_2[n' + n']
    rewrite IH
  }
end

theorem 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 rewrite add_zero[n]
  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_aux}
  }
  case suc(n') suppose IH {
    suffices suc(div2(n' + suc(n'))) = suc(n')  by definition {operator+, div2, div2_aux}
    suffices suc(div2(suc(n' + n'))) = suc(n')  by rewrite add_suc[n'][n']
    rewrite IH
  }
end

theorem 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 rewrite add_zero[n]
  div2_suc_double[n]
end

/*
 Properties of pos2nat
 */

theorem pos_positive: all p:Pos. 0 < pos2nat(p)
proof
  induction Pos
  case one {
    definition {pos2nat, operator<, operator≤, operator≤}
  }
  case succ(p') {
    definition {pos2nat, operator<, operator≤, operator≤}
  }
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 rewrite pn_s
    suffices 0 < suc(pn') + (suc(pn') + 0)  by definition {operator*,operator*,operator*}
    suffices 0 < suc(pn') + suc(pn')  by rewrite add_zero[suc(pn')]
    suffices 0 < suc(pn' + suc(pn'))  by definition operator+
    suffices 0 < suc(suc(pn' + pn'))  by rewrite add_suc[pn'][pn']
    definition {operator<, operator≤, operator≤}
  }
end

/*
 Properties of Division and Modulo
 */

lemma find_quotient_correct: all u:Nat. all q:Nat, n:Nat, m:Pos.
  if q * pos2nat(m) ≤ n and n < u * pos2nat(m)
  then some r : Nat. find_quotient(u, n, m, q) * pos2nat(m) + r = n
                     and r < pos2nat(m)
proof
  induction Nat
  case zero {
    arbitrary q:Nat, n:Nat, m:Pos
    suppose prem
    conclude false
      by definition {operator*, operator <, operator ≤} in prem
  }
  case suc(u') suppose IH {
    arbitrary q:Nat, n:Nat, m:Pos
    suppose prem
    have n_sn: n ≤ suc(n)   by less_equal_suc[n]
    _definition find_quotient
    switch suc(q) * pos2nat(m) ≤ n {
      case true suppose sqm_le_n {
        have sqm_le_n: suc(q) * pos2nat(m) ≤ n  by rewrite sqm_le_n
        switch n < u' * pos2nat(m) {
          case true suppose n_l_um_true {
            have n_l_um: n < u' * pos2nat(m)    by rewrite n_l_um_true
            have IH_sq: some r:Nat.
                   find_quotient(u',n,m,suc(q)) * pos2nat(m) +r = n
                   and r < pos2nat(m)
            by apply IH[suc(q),n,m] to sqm_le_n, n_l_um
            obtain r where Q: find_quotient(u',n,m,suc(q)) * pos2nat(m) + r = n
                   and r < pos2nat(m) from IH_sq
            choose r
            Q
          }
          case false suppose n_l_um_false {
            define M = pos2nat(m)
            define R = n - u' * M
            choose R
	    have um_le_n: u' * M ≤ n
	      by have not_n_l_um: not (n < u' * M)
	           by suffices not (n < u' * pos2nat(m))  by definition M
                      suppose p rewrite (definition M in n_l_um_false) in p
		 apply not_less_less_equal to not_n_l_um
	    have um_r_eq_n: u' * M + R = n
	      by suffices u' * M + (n - u' * M) = n  by definition R
	         apply sub_add_identity[n][u' * M] to um_le_n
	    have r_l_m: R < M
	      by suffices suc(n - u' * M) ≤ M  by definition {R, operator<}
	         have sn_le_um_m: suc(n) ≤ (u' * M) + M
		   by suffices suc(n) ≤ M + u' * M  by rewrite add_commute[u' * M][M]
                      suffices suc(n) ≤ pos2nat(m) + u' * pos2nat(m)  by definition M
		      definition {operator <, operator*, M} in prem
		 have um_le_sn: u' * M ≤ suc(n)
		   by apply less_equal_trans to um_le_n, n_sn
		 have sn_um_le_m: suc(n) - (u' * M) ≤ M
		   by apply less_equal_add_sub[suc(n)][u' * M, M]
		      to um_le_sn, sn_le_um_m
	         conclude suc(n - u' * M) ≤ M
		   by have eq: suc(n - u' * M) = suc(n) - u' * M
		        by definition {operator+,operator+} in
    		           apply sub_add_assoc[n][1, u'*M] to um_le_n
	              suffices suc(n) - u' * M ≤ M  by rewrite eq
                      sn_um_le_m
            um_r_eq_n, r_l_m
          }
        }
      }
      case false suppose sqn_g_n {
        define M = pos2nat(m)
        define R = n - q * M
        
        have qm_le_sn: q * M ≤ suc(n)
          by have qm_le_n: q * M ≤ n
               by suffices q * pos2nat(m) ≤ n  by definition M
                  definition M in prem
             apply less_equal_trans to qm_le_n, n_sn
        have sn_le_qm_m: suc(n) ≤ q * M + M
          by have not_sqm_le_n: not (suc(q) * M ≤ n)
                 by suppose p rewrite sqn_g_n in p
             have n_l_sqm: n < suc(q) * M
                 by apply not_less_equal_greater to not_sqm_le_n
             rewrite add_commute[M][q*M] in
             definition {operator<,operator*} in n_l_sqm
        have sn_qm_le_m: suc(n) - q * M ≤ M
          by apply less_equal_add_sub to qm_le_sn, sn_le_qm_m
        have qm_le_n: q * M ≤ n   by suffices q * pos2nat(m) ≤ n  by definition M
                                     definition M in prem
        have s_nqm_le_m: suc(n - q * M) ≤ M
          by have eq: 1 + (n - q * M) = (1 + n) - q * M
               by apply sub_add_assoc[n][1,q*M] to qm_le_n
             have eq2: suc(n - q * M) = suc(n) - q * M
               by definition {operator+,operator+} in eq
             suffices suc(n) - q * M ≤ M  by rewrite eq2
             sn_qm_le_m
        have nqm_l_m: R < M
          by suffices suc(n - q * M) ≤ M  by definition {R,operator<}
             s_nqm_le_m

        have qm_r_eq_n: q * M + R = n
          by suffices q * M + (n - q * M) = n  by definition R
             apply sub_add_identity to qm_le_n
          
        choose n - q * M
        enable {R,M} qm_r_eq_n, nqm_l_m
      }
    }
  }
end

theorem mod_def: all n:Nat, m:Pos.
  n % m = n - (n / m) * pos2nat(m)
proof
  arbitrary n:Nat, m:Pos
  switch n {
    case 0 {
      definition {operator-,operator%}
    }
    case suc(n') {
      definition {operator%}
    }
  }
end

theorem division: all n:Nat, m:Pos.
  some r : Nat. (n / m) * pos2nat(m) + r = n  and  r < pos2nat(m)
proof
  arbitrary n:Nat, m:Pos
  switch n {
    case 0 {
      choose 0
      suffices 1 ≤ pos2nat(m)  by definition {operator/, operator*, operator+, operator<}
      definition operator< in pos_positive[m]
    }
    case suc(n') suppose n_sn {
      have qm_le_n: 0 * pos2nat(m) ≤ n
	by definition {operator*,operator≤}
      define u = suc(n) * pos2nat(m)
      have n_l_um: n < u * pos2nat(m)
        by suffices suc(n) ≤ (pos2nat(m) + n * pos2nat(m)) * pos2nat(m)
              by definition {operator<, u, operator*}
	   switch m {
	     case one {
               suffices suc(n) ≤ suc(n * 1) * 1    by definition {pos2nat, operator+, operator+}
	       suffices suc(n) ≤ suc(n * 1)        by rewrite mult_one[suc(n * 1)]
	       suffices suc(n) ≤ suc(n)            by rewrite mult_one[n]
	       less_equal_refl[suc(n)]
	     }
	     case succ(m') suppose m_sm {
	       suffices suc(n) ≤ (suc(pos2nat(m')) + n * suc(pos2nat(m'))) * suc(pos2nat(m'))
                 by definition pos2nat
               define M = pos2nat(m')
               suffices n ≤ M + (M + n * suc(M)) * suc(M)
                  by definition {operator+, operator*, operator+, operator≤}
               have eq: M + (M + n * suc(M)) * suc(M)
                      = n + ((M * n + M) + (M * ((n + M * n) + M) + M)) 
                 by equations M + (M + n * suc(M)) * suc(M)
                           = (M + n * suc(M)) * suc(M) + M    by add_commute[M][(M + n * suc(M)) * suc(M)]
                       ... = (M + suc(M) * n) * suc(M) + M    by rewrite mult_commute[n][suc(M)]
                       ... = (M + (n + M * n)) * suc(M) + M   by rewrite suc_mult[M,n]
                       ... =  ((n + M * n) + M) * suc(M) + M  by rewrite add_commute[M][n + M*n]
                       ... = suc(M) * ((n + M * n) + M) + M
                                      by rewrite mult_commute[((n + M * n) + M)][suc(M)]
                       ... = (((n + M * n) + M) + M * ((n + M * n) + M)) + M  by definition operator*
                       ... = ({n + M * n + M} + M * ((n + M * n) + M)) + M
                                 by rewrite symmetric add_assoc[n][M*n,M]
                       ... = (n + (M * n + M)) + (M * ((n + M * n) + M) + M)
                                      by rewrite add_assoc[(n + M * n + M)][M * ((n + M * n) + M),M]
                       ... = n + ((M * n + M) + (M * ((n + M * n) + M) + M))
                                      by rewrite add_assoc[n][(M * n + M), (M * ((n + M * n) + M) + M)]
               suffices n ≤ n + ((M * n + M) + (M * ((n + M * n) + M) + M))
                 by rewrite eq
               less_equal_add[n][((M * n + M) + (M * ((n + M * n) + M) + M))]
	     }
	   }
      have fqc: some r:Nat. find_quotient(u, n, m, 0) * pos2nat(m) + r = n
                    and r < pos2nat(m)
        by apply find_quotient_correct[u][0, n, m] to qm_le_n, n_l_um
      obtain r where R: find_quotient(u, n, m, 0) * pos2nat(m) + r = n
			and r < pos2nat(m)
	  from fqc
      choose r
      suffices find_quotient(suc(suc(n')) * pos2nat(m),suc(n'),m,0) * pos2nat(m) + r = suc(n') and r < pos2nat(m)
        by definition operator/
      suffices find_quotient(suc(n) * pos2nat(m),n,m,0) * pos2nat(m) + r = n and r < pos2nat(m)
        by rewrite symmetric n_sn
      definition u in R
    }
  }
end

theorem division_remainder: all n:Nat, m:Pos.
  (n / m) * pos2nat(m) + (n % m) = n
proof
  arbitrary n:Nat, m:Pos
  suffices (n / m) * pos2nat(m) + (n - (n / m) * pos2nat(m)) = n
      by rewrite mod_def[n,m]
  define a = (n / m) * pos2nat(m)
  obtain r where R: (n / m) * pos2nat(m) + r = n and r < pos2nat(m)
    from division[n, m]
  have ar_n: a + r = n   by _definition a R
  have a_le_a_r: a ≤ a + r  by less_equal_add[a][r]
  have n_eq_a_r: n = a + r
    by _definition a symmetric conjunct 0 of R
  have a_le_n: a ≤ n   by _rewrite n_eq_a_r a_le_a_r
  conclude a + (n - a) = n
    by apply sub_add_identity to a_le_n
end

theorem remainder_less_divisor: all n:Nat, m:Pos.
  n % m < pos2nat(m)
proof
  arbitrary n:Nat, m:Pos
  suffices n - (n / m) * pos2nat(m) < pos2nat(m)
      by rewrite mod_def[n,m]
  define a = (n / m) * pos2nat(m)
  obtain r where R: (n / m) * pos2nat(m) + r = n and r < pos2nat(m)
    from division[n, m]
  have ar_n: a + r = n   by _definition a R
  have ar_a_a: (a + r) - a = r  by add_sub_identity[a][r]
  have r_na: r = n - a  by _rewrite symmetric ar_n symmetric ar_a_a
  suffices r < pos2nat(m)   by rewrite symmetric r_na
  conjunct 1 of R
end

/*
theorem div_one: all n:Nat.
  n / one = n
proof
  arbitrary n:Nat
  switch n {
    case zero {
      definition operator/
    }
    case suc(n') {
      _definition operator/
      sorry
    }
  }
end
*/