Less-than is irreflexive on naturals
Closed
Theorem & proof
·
nat_lt_irrefl.lean
·
✓ verified
1
2
3
import Mathlib theorem nat_lt_irrefl (n : Nat) : ¬ (n < n) := by lia
Rewards pledged
No rewards pledged yet.