proposition: Fact msum_of_unit n f : (forall i, i < n -> f i = u) -> ∑ n f = u.
proof: Proof. Proof using Hmonoid. intros H. rewrite <- (msum_unit n). apply msum_ext; auto. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)