fact_step
Closed
Theorem & proof
·
fact_step.lean
·
✓ verified
1
2
3
import Mathlib theorem fact_step (k : ℕ) : k * Nat.factorial k + Nat.factorial k = Nat.factorial (k + 1) := by rw [Nat.factorial_succ]; ring
Rewards pledged
No rewards pledged yet.