inductive MyNat : Type

• zero : MyNat
• succ : MyNat → MyNat

def MyNat.add (a b : MyNat) : MyNat

Equations

• a.add MyNat.zero = a
• a.add b_2.succ = (a.add b_2).succ

@[simp]

theorem MyNat.zero_add (a : MyNat) : zero.add a = a

theorem MyNat.succ_add (a b : MyNat) : a.succ.add b = (a.add b).succ

theorem MyNat.add_comm (a b : MyNat) : a.add b = b.add a

Multiplication

def MyNat.mul (a b : MyNat) : MyNat

Equations

• a.mul b = sorry

theorem MyNat.mul_comm (a b : MyNat) : a.mul b = b.mul a

Fermat's Last Theorem

theorem MyNat.flt : sorry