Successor is injective
Closed
Theorem & proof
·
nat_succ_injective.lean
·
✓ verified
1
2
3
import Mathlib theorem nat_succ_injective {m n : Nat} (h : m + 1 = n + 1) : m = n :=Nat.succ.inj h
Rewards pledged
No rewards pledged yet.