Successor of natural is non-zero
Closed
Theorem & proof
·
nat_succ_ne_zero.lean
·
✓ verified
1
2
3
import Mathlib theorem nat_succ_ne_zero (n : Nat) : n + 1 ≠ 0 :=Nat.succ_ne_zero n
Rewards pledged
No rewards pledged yet.