proposition: Lemma horner0 p x : (forall n, nth p n = 0%R) -> p.[x] = 0%R.
proof: Proof. by move=> Hp; rewrite hornerE big1 // =>[i _]; rewrite Hp Rmult_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