8 lines
119 B
Lean4
8 lines
119 B
Lean4
import Mathlib
|
||
|
||
|
||
theorem demo (n : ℕ) : n + 0 = n := by
|
||
induction n with
|
||
| zero => rfl
|
||
| succ n ih => simp_all
|