proposition: Lemma mcoeffMX p m k : (p * 'X_[m])@_(m + k) = p@_k.
proof: Proof. rewrite commr_mpolyX mpolyME msuppX big_allpairs. rewrite big_seq1 [X in _=X@__]mpolyE !raddf_sum /=. by apply/eq_bigr=> i _; rewrite !mcoeffZ !mcoeffX eqxx mul1r eqm_add2l. 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