proposition: Lemma horner_opp p x : horner tt (opp p) x = Ropp (horner tt p x).
proof: Proof. rewrite !hornerE size_opp. rewrite big_endo ?Ropp_0 //; last exact: Ropp_plus_distr. apply: eq_bigr => i _ /=. by rewrite nth_opp Ropp_mult_distr_l_reverse. Qed.
imports: Coq(ZArith Reals) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Flocq(Core) Stdlib MathComp Interval Xreal Basic_rec