proposition: Lemma poly_mulA : associative mpoly_mul.
proof: Proof. move=> p q r; apply/mpolyP=> mi; pose_big_enough b. rewrite (mcoeff_pml b) // (mcoeff_pmlr b) //. 2: by close. have h m: !|mi - m| < b by exact/(leq_ltn_trans (mdegB mi m)). pose coef3 mj mk := p@_mj * (q@_(mi - mj - mk)%MM * r@_mk). transitivity (\sum_(mj : 'X_{1..n < b} | (mj <= mi)%MM) \sum_(mk : 'X_{1..n < b} | (mk <= mi - mj)%MM) coef3 mj mk). by apply/eq_bigr=> /= mj _; rewrite (mcoeff_pmlr b) 1?big_distrr. pose P (mj : 'X_{1..n < b}) := (mj <= mi)%MM. rewrite (exchange_big_dep P) //= {}/P; last first. by move=> mj mk _ /lepm_trans; apply; apply/lem_subr. apply/eq_bigr=> /= mk /mnm_lepP le_mk_mi. transitivity (\sum_(mj : 'X_{1..n < b} | (mj <= mi - mk)%MM) coef3 mj mk). + apply/eq_bigl=> m /=. apply/idP/idP => [/andP[/mnm_lepP le1 /mnm_lepP le2]|le1]. * apply/mnm_lepP => i; rewrite mnmBE /leq subnBA // addnC -subnBA //. by rewrite -mnmBE; apply/le2. * have le2: (m <= mi)%MM by rewrite (lepm_trans le1) ?lem_subr. rewrite le2; apply/mnm_lepP=> i; rewrite mnmBE /leq. move/mnm_lepP: le2 => le2; rewrite subnBA // addnC. by rewrite -subnBA //; move/mnm_lepP/(_ i): le1; rewrite mnmBE. rewrite (mcoeff_pml b) /coef3 1?big_distrl //=. by apply/eq_bigr=> mj le_mj_miBk; rewrite !mulrA !submDA 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