proposition: Lemma mwidenE (p : {mpoly R[n]}) (k : nat) : msize p <= k -> mwiden p = \sum_(m : 'X_{1..n < k}) (p@_m *: 'X_[mnmwiden m]).
proof: Proof. move=> h; rewrite {1}[p](mpolywE (k := k)) //. rewrite raddf_sum /=; apply/eq_bigr=> m _. by rewrite mwidenZ mwidenX. 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