proposition: Lemma horner_lift n p x : horner tt (lift n p) x = (horner tt p x * x ^ n)%R.
proof: Proof. rewrite !hornerE . rewrite (big_endo (fun y => y * x ^ n)%R); first last. by rewrite Rmult_0_l. by red=> *; rewrite Rmult_plus_distr_r. rewrite size_lift. rewrite (@big_cat_nat _ _ _ n) ?leq_addr //=. rewrite big1_seq; first last. move=> i /andP [_ Hi]; rewrite nth_lift ifT ?Rmult_0_l //. by move: Hi; rewrite mem_index_iota; case/andP. rewrite Rplus_0_l -{1}(add0n n) big_addn addKn. apply: eq_bigr => i _ /=. rewrite nth_lift ifF ?(ltnNge, leq_addl) //. rewrite addnK Rmult_assoc; congr Rmult. by rewrite pow_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