Theorem: IMOSL.IMO2006N3.g_eq_sum_divisors_card (IMOSLLean4/IMO2006/N3/N3.lean)

State before:
⊢ g 0 = ∑ k ∈ range 0, k.succ.divisors.card
Tactic:
rw [sum_range_zero, g_zero]
State after:
no goals

State before:
n : ℕ
⊢ g (n + 1) = ∑ k ∈ range (n + 1), k.succ.divisors.card
Tactic:
rw [g_succ, sum_range_succ, ← g_eq_sum_divisors_card]
State after:
no goals