proposition: Lemma comp_polyE p q : p \Po q = \sum_(i < size p) p`_i *: q^+i.
proof: Proof. by rewrite [p \Po q]horner_poly; apply: eq_bigr => i _; rewrite mul_polyC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)