proposition: Fact msum_1 f : ∑ 1 f = f 0.
proof: Proof. Proof using Hmonoid. destruct Hmonoid as [ H1 H2 ]. rewrite msum_S, msum_0, H2; auto. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)