proposition: Lemma horner_propagate u pi : J.propagate (horner u pi).
proof: Proof. intros x. apply I.mask_propagate_r. 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