proposition: Lemma mwidenX m : mwiden 'X_[m] = 'X_[mnmwiden m].
proof: Proof. rewrite /mwiden mmapX /mmap1 /= (mpolyXE _ 1); apply/esym. rewrite (eq_bigr (fun i => 'X_i ^+ (mnmwiden m i))); last first. by move=> i _; rewrite perm1. rewrite big_ord_recr /= mnmwiden_ordmax expr0 mulr1. by apply/eq_bigr=> i _; rewrite mnmwiden_widen. 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