Theorem: Fin.sum_succ (GMLInit/Data/Fin/Basic.lean)

State before:
n : Nat
α : Type u_1
inst✝¹ : Add α
inst✝ : OfNat α 0
f : Fin (n + 1) → α
⊢ sum f = f 0 + sum (f ∘ succ)
Tactic:
simp [sum, foldr_succ]
State after:
no goals