proposition: Fact mscal_mult a b x : mscal (a*b) x = mscal a (mscal b x).
proof: Proof. Proof using Hmonoid. induction a as [ | a IHa ]; simpl. + do 2 rewrite mscal_0; auto. + rewrite mscal_plus, IHa, mscal_S; auto. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)