proposition: Lemma mpolywME p q k : msize p <= k -> msize q <= k -> p * q = \sum_(m : 'X_{1..n < k, k}) (p@_m.1 * q@_m.2) *: 'X_[m.1 + m.2].
proof: Proof. move=> ltpk ltqk; rewrite mpolyME; pose I : subFinType _ := 'X_{1..n < k}. rewrite big_allpairs (big_mksub I) /=; last first. by move=> m /msize_mdeg_lt /leq_trans; apply. by rewrite msupp_uniq. rewrite big_rmcond /= => [|i]; last first. by move/memN_msupp_eq0=> ->; rewrite big1 // => j _; rewrite mul0r scale0r. rewrite big_pairA /=; apply/eq_bigr=> i _; rewrite (big_mksub I)/=; last first. - by move=> m /msize_mdeg_lt /leq_trans; apply. - by rewrite msupp_uniq. rewrite big_rmcond /= => [//|j]. by move/memN_msupp_eq0=> ->; rewrite mulr0 scale0r. 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