proposition: Fact msum_plus1 n f : ∑ (S n) f = ∑ n f ⊕ f n.
proof: Proof. Proof using Hmonoid. destruct Hmonoid as [ _ H2 _ ]. replace (S n) with (n+1) by lia. rewrite msum_plus; simpl; f_equal. rewrite H2; f_equal; lia. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)