proposition: Lemma toSeq_horner0 (u : U) (p : T) : horner u p 0%R = head 0%R (toSeq p).
proof: Proof. elim: p=> [| a q HI] ; first by []. by rewrite /= HI; case: u HI; rewrite Rmult_0_r Rplus_0_l. 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