theorem Fin.sum_univ_castSucc' {M : Type u_1} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) : ∑ i : Fin n, f i.castSucc = ∑ i < last n, f i