proposition: Fact mscal_1 x : mscal 1 x = x.
proof: Proof. Proof using Hmonoid. destruct Hmonoid as [ _ H2 _ ]. rewrite mscal_S, mscal_0, H2; trivial. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)