 151    show succ n + succ m = succ (n + succ m)
 152    rw [add_succ, add_succ, ih]
 153
 154theorem add_assoc (a b c : LogicNat) : (a + b) + c = a + (b + c) := by
 155  induction c with
 156  | identity => rfl
 157  | step c ih =>
 158    show (a + b) + succ c = a + (b + succ c)
 159    rw [add_succ, add_succ, add_succ, ih]
 160
 161theorem add_comm (a b : LogicNat) : a + b = b + a := by
 162  induction b with
 163  | identity =>
 164    show a + zero = zero + a
 165    rw [add_zero, zero_add]
 166  | step b ih =>
 167    show a + succ b = succ b + a
 168    rw [add_succ, succ_add, ih]
 169
 170/-- Multiplication by recursion on the second argument. -/
 171def mul : LogicNat → LogicNat → LogicNat
 172  | _, .identity => zero
 173  | n, .step m   => mul n m + n
 174
 175instance : Mul LogicNat := ⟨mul⟩
 176
 177@[simp] theorem mul_def (n m : LogicNat) : n * m = mul n m := rfl
 178
 179@[simp] theorem mul_zero (n : LogicNat) : n * zero = zero := rfl
 180
 181@[simp] theorem mul_succ (n m : LogicNat) : n * succ m = n * m + n := rfl
 182
 183theorem zero_mul (n : LogicNat) : zero * n = zero := by
 184  induction n with

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.