proposition: Fact mscal_plus a b x : mscal (a+b) x = mscal a x ⊕ mscal b x.
proof: Proof. Proof using Hmonoid. apply msum_plus. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)