proposition: Fact mscal_morph n x : phi (mscal m1 u1 n x) = mscal m2 u2 n (phi x).
proof: Proof. Proof using Hphi1 Hphi2. apply msum_morph. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)