Successor of a natural is positive
Closed
Theorem & proof
·
nat_succ_pos.lean
·
✓ verified
1
2
3
import Mathlib theorem nat_succ_pos (n : Nat) : 0 < n + 1 := by omega
Rewards pledged
No rewards pledged yet.