proposition: Fact coef_mul_poly_rev p q i : (mul_poly p q)`_i = \sum_(j < i.+1) p`_(i - j)%N * q`_j.
proof: Proof. rewrite coef_mul_poly (reindex_inj rev_ord_inj) /=. by apply: eq_bigr => j _; rewrite (sub_ordK j). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)