proposition: Lemma hornerN p x : (- p).[x] = - p.[x].
proof: Proof. rewrite -[-%R]/opp_poly unlock horner_poly horner_coef -sumrN /=. by apply: eq_bigr => i _; rewrite mulNr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)