Adding zero on the left
Closed
Theorem & proof
·
nat_zero_add.lean
·
✓ verified
1
2
3
4
import Mathlib theorem nat_zero_add (n : Nat) : 0 + n = n := Nat.rec rfl (fun _ => congrArg Nat.succ) n
Rewards pledged
No rewards pledged yet.