Less-than is transitive on naturals
Closed
Theorem & proof
·
nat_lt_trans.lean
·
✓ verified
1
2
3
import Mathlib theorem nat_lt_trans {a b c : Nat} (h₁ : a < b) (h₂ : b < c) : a < c :=Nat.lt_trans h₁ h₂
Rewards pledged
No rewards pledged yet.