proposition: Lemma hornerD p q x : (p + q).[x] = p.[x] + q.[x].
proof: Proof. rewrite -[+%R]/(@add_poly R) unlock horner_poly; set m := maxn _ _. rewrite !(@horner_coef_wide m) ?leq_max ?leqnn ?orbT // -big_split /=. by apply: eq_bigr => i _; rewrite -mulrDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)