proposition: Lemma msuppMCX c m : c != 0 -> msupp (c *: 'X_[m]) = [:: m].
proof: Proof. move=> nz_c; rewrite -mul_mpolyC; apply/perm_small_eq=> //. by rewrite (permPl (msuppMX _ _)) msuppC (negbTE nz_c) /= addm0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg