proposition: Fact msum_plus a b f : ∑ (a+b) f = ∑ a f ⊕ ∑ b (fun i => f (a+i)).
proof: Proof. Proof using Hmonoid. destruct Hmonoid as [ H1 _ H3 ]. revert f; induction a as [ | a IHa ]; intros f; simpl; auto. rewrite <- H3; f_equal; apply IHa. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)