Addition is associative on the naturals
Closed
Theorem & proof
·
nat_add_assoc.lean
·
✓ verified
1
2
3
import Mathlib theorem nat_add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) :=Nat.add_assoc a b c
Rewards pledged
No rewards pledged yet.