proposition: Lemma mcoeff_poly_mul_lin_rev p q m k : !|m| < k -> (p *M q)@_m = \sum_(k : 'X_{1..n < k} | (k <= m)%MM) p@_(m-k) * q@_k.
proof: Proof. move=> /[dup] /mcoeff_pml -> lt. have pr (h : 'X_{1..n}) : !|m - h| < k by exact: leq_ltn_trans (mdegB _ _) _. pose F (k : 'X_{1..n < k}) := BMultinom (pr k). have inv_F (h : 'X_{1..n}): (h <= m)%MM -> (m - (m - h))%MM = h. by move=> le_hm; rewrite submBA // addmC addmK. rewrite (reindex_onto F F) //=; last first. by move=> h /inv_F eqh; apply/eqP; rewrite eqE /= eqh. apply/esym/eq_big => [h /=|h /inv_F -> //]; apply/esym; rewrite lem_subr eqE /=. by apply/eqP/idP => [<-|/inv_F //]; apply/mnm_lepP=> i; rewrite !mnmBE leq_subr. 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