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