proposition: Lemma msuppMX p m : perm_eq (msupp (p * 'X_[m])) [seq (m + m')%MM | m' <- msupp p].
proof: Proof. apply/uniq_perm=> //; first rewrite map_inj_uniq //. by move=> m1 m2 /=; rewrite ![(m + _)%MM]addmC; apply: addIm. move=> m'; apply/idP/idP; last first. case/mapP=> mp mp_in_p ->; rewrite mcoeff_msupp. by rewrite mcoeffMX -mcoeff_msupp. move/msuppM_le; rewrite msuppX => /allpairsP [[p1 p2]] /=. rewrite mem_seq1; case=> p1_in_p /eqP <- ->. by apply/mapP; exists p1; last rewrite addmC. 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