proposition: Lemma mwiden_mnmwiden p m : (mwiden p)@_(mnmwiden m) = p@_m.
proof: Proof. rewrite (mwidenE (k := msize p)) // raddf_sum /=. rewrite [X in _=X@__](mpolywE (k := msize p)) //. rewrite raddf_sum /=; apply/eq_bigr=> i _. by rewrite !mcoeffZ !mcoeffX inj_eq //; apply/inj_mnmwiden. 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