proposition: Lemma horner_crealP (p : {poly F}) (x : creal) : creal_axiom (fun i => p.[x i]).
proof: Proof. exists_big_modulus m F=> [e i j e_gt0 hi hj|]. rewrite (le_lt_trans (@poly_accr_bound1P _ p (x (cauchymod x 1)) 1 _ _ _ _)); do ?[by rewrite ?e_gt0 | by rewrite ltW // cauchymodP]. rewrite -ltr_pdivl_mulr ?poly_accr_bound_gt0 ?cauchymodP //. by rewrite pmulr_rgt0 ?invr_gt0 ?poly_accr_bound_gt0. by close. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)