proposition: Lemma mcoeffMr p q m : (p * q)@_m = \sum_(k : 'X_{1..n < !|m|.+1, !|m|.+1} | m == (k.1 + k.2)%MM) (p@_k.2 * q@_k.1).
proof: Proof. rewrite mcoeffM big_cond_mulrn big_pairA/=. rewrite exchange_big pair_bigA /= -big_cond_mulrn. by apply: eq_bigl=> k /=; rewrite addmC. 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