proposition: Lemma horner_correct u pi ai p a : pi >:: p -> ai >: a -> horner u pi ai >: PolR.horner tt p a.
proof: Proof. move=> Hp Ha. rewrite /horner /PolR.horner. apply: I.mask_correct'. apply: (foldr_correct (Rel := fun v t => t >: v)) =>//. - exact: J.zero_correct. - move=> x y /J.contains_only_0 -> /J.contains_only_0 ->; rewrite Rmult_0_l Rplus_0_r; exact: J.zero_correct. - move=> x y Hx Hy; rewrite -(Rplus_0_r 0) -{1}(Rmult_0_l a). apply: J.add_correct =>//; exact: J.mul_correct. - move=> x xi y yi Hx Hy; apply: J.add_correct=>//; exact: J.mul_correct. 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