proposition: Lemma mcoeff_poly_mul p q m k : !|m| < k -> (p *M q)@_m = \sum_(k : 'X_{1..n < k, k} | m == (k.1 + k.2)%MM) p@_k.1 * q@_k.2.
proof: Proof. pose_big_enough i; first rewrite (mpoly_mulwE i i) // => lt_mk. rewrite mcoeff_MPoly raddf_sum /=; have lt_mi: k < i by []. apply/esym; rewrite big_cond_mulrn !big_pairA /=. pose Ik : subFinType _ := 'X_{1..n < k}. pose Ii : subFinType _ := 'X_{1..n < i}. pose F i j := (p@_i * q@_j) *+ (m == (i + j))%MM. pose G i := \sum_(j : 'X_{1..n < k}) (F i j). rewrite (big_sub_widen Ik Ii xpredT G) /=; last first. by move=> x /leq_trans; apply. rewrite big_rmcond /=; last first. case=> /= j _; rewrite -leqNgt => /(leq_trans lt_mk) h. rewrite {}/G {}/F big1 // => /= l _. case: eqP h => [{1}->|]; last by rewrite mulr0n. by rewrite mdegD ltnNge leq_addr. apply/eq_bigr=> j _; rewrite {}/G. rewrite (big_sub_widen Ik Ii xpredT (F _)) /=; last first. by move=> x /leq_trans; apply. rewrite big_rmcond => //=; last first. move=> l; rewrite -leqNgt => /(leq_trans lt_mk) h. rewrite {}/F; case: eqP h; rewrite ?mulr0n //. by move=> ->; rewrite mdegD ltnNge leq_addl. by apply/eq_bigr=> l _; rewrite {}/F coeffU eq_sym mulr_natr. by close. 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