proposition: Lemma mpoly_mulwE p q kp kq : msize p <= kp -> msize q <= kq -> p *M q = [mpoly \sum_(m : 'X_{1..n < kp, kq}) p *M_[m] q].
proof: Proof. pose Ip : subFinType _ := 'X_{1..n < kp}. pose Iq : subFinType _ := 'X_{1..n < kq}. move=> lep leq; apply/mpoly_eqP/esym=> /=. rewrite big_allpairs/= big_pairA. rewrite (big_mksub Ip) ?msupp_uniq //=; first last. by move=> x /msize_mdeg_lt /leq_trans; apply. rewrite [X in _ = X]big_rmcond /=; last first. move=> i /memN_msupp_eq0 ->; rewrite big1=> //. by move=> j _; rewrite mul0r freegU0. apply/eq_bigr=> i _; rewrite (big_mksub Iq) /=; first last. by move=> x /msize_mdeg_lt /leq_trans; apply. by rewrite msupp_uniq. rewrite [X in _ = X]big_rmcond //= => j /memN_msupp_eq0 ->. by rewrite mulr0 freegU0. 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