proposition: Lemma horner_add p q x : horner tt (add tt p q) x = (horner tt p x + horner tt q x)%R.
proof: Proof. rewrite !(@hornerE_wide (maxn (size p) (size q))). rewrite -big_split; apply: eq_bigr => i _ /=. by rewrite nth_add Rmult_plus_distr_r. exact: leq_maxr. exact: leq_maxl. by rewrite size_add. 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