proposition: Fact msum_mscal n k f : (forall i j, i < n -> j < n -> f i ⊕ f j = f j ⊕ f i) -> ∑ n (fun i => mscal k (f i)) = mscal k (∑ n f).
proof: Proof. Proof using Hmonoid. intros H; apply msum_msum; auto. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)