proposition: Fact msum_ends n f : (forall i, 0 < i <= n -> f i = u) -> ∑ (n+2) f = f 0 ⊕ f (S n).
proof: Proof. Proof using Hmonoid. destruct Hmonoid as [ H1 H2 H3 ]. intros H. replace (n+2) with (1 + n + 1) by lia. do 2 rewrite msum_plus; simpl. rewrite msum_of_unit. + rewrite H2, H2, H2; do 2 f_equal; lia. + intros; apply H; lia. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)