theorem
proved
add_succ
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.ArithmeticFromLogic on GitHub at line 138.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
135
136@[simp] theorem add_zero (n : LogicNat) : n + zero = n := rfl
137
138@[simp] theorem add_succ (n m : LogicNat) : n + succ m = succ (n + m) := rfl
139
140theorem zero_add (n : LogicNat) : zero + n = n := by
141 induction n with
142 | identity => rfl
143 | step n ih =>
144 show zero + succ n = succ n
145 rw [add_succ, ih]
146
147theorem succ_add (n m : LogicNat) : succ n + m = succ (n + m) := by
148 induction m with
149 | identity => rfl
150 | step m ih =>
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]