proposition: Lemma mcoeff_poly_mul_lin p q m k : !|m| < k -> (p *M q)@_m = \sum_(k : 'X_{1..n < k} | (k <= m)%MM) p@_k * q@_(m-k).
proof: Proof. move=> lt_m_k; rewrite (mcoeff_poly_mul _ _ (k := k)) //. pose P (k1 k2 : 'X_{1..n < k}) := m == (k1 + k2)%MM. pose Q (k : 'X_{1..n < k}) := (k <= m)%MM. pose F (k1 k2 : 'X_{1..n}) := p@_k1 * q@_k2. rewrite -(pair_big_dep xpredT P F) (bigID Q) /= addrC. (rewrite big1 ?add0r {}/P {}/Q; first apply/eq_bigr)=> /= h1. + move=> le_h1_m; have pr: !|m - h1| < k. by rewrite (leq_ltn_trans _ lt_m_k) // mdegB. rewrite (big_pred1 (BMultinom pr)) //= => h2 /=. rewrite bmeqP /=; apply/eqP/eqP=> ->. * by rewrite addmC addmK. * by rewrite addmC submK //; apply/mnm_lepP. + rewrite negb_forall => /existsP /= [i Nle]. rewrite big_pred0 //= => h2; apply/negbTE/eqP. move/mnmP/(_ i); rewrite mnmDE=> eq; move: Nle. by rewrite eq leq_addr. 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