proposition: Fact msum_unit n : ∑ n (fun _ => u) = u.
proof: Proof. Proof using Hmonoid. destruct Hmonoid as [ H1 _ _ ]. induction n as [ | n IHn ]; simpl; auto. rewrite IHn; auto. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)