proposition: Fact mul_polyA : associative mul_poly.
proof: Proof. move=> p q r; apply/polyP=> i; rewrite coef_mul_poly coef_mul_poly_rev. pose coef3 j k := p`_j * (q`_(i - j - k)%N * r`_k). transitivity (\sum_(j < i.+1) \sum_(k < i.+1 | k <= i - j) coef3 j k). apply: eq_bigr => /= j _; rewrite coef_mul_poly_rev big_distrr /=. by rewrite (big_ord_narrow_leq (leq_subr _ _)). rewrite (exchange_big_dep predT) //=; apply: eq_bigr => k _. transitivity (\sum_(j < i.+1 | j <= i - k) coef3 j k). apply: eq_bigl => j; rewrite -ltnS -(ltnS j) -!subSn ?leq_ord //. by rewrite -subn_gt0 -(subn_gt0 j) -!subnDA addnC. rewrite (big_ord_narrow_leq (leq_subr _ _)) coef_mul_poly big_distrl /=. by apply: eq_bigr => j _; rewrite /coef3 -!subnDA addnC mulrA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)