proposition: Lemma horner2_crealP (p : {poly {poly F}}) (x y : creal) : creal_axiom (fun i => p.[x i, y i]).
proof: Proof. set a := x (cauchymod x 1). exists_big_modulus m F. move=> e i j e_gt0 hi hj; rewrite (@split_dist_add p.[x i, y j]) //. rewrite (le_lt_trans (@poly_accr_bound1P _ _ 0 (ubound y) _ _ _ _)) //; do ?by rewrite ?subr0 ?uboundP. apply: le_lt_trans (_ : `|y i - y j| * bound_poly_accr_bound x p 0 (ubound y) < _). by rewrite ler_wpmul2l ?normr_ge0 // bound_poly_accr_boundP. rewrite -ltr_pdivl_mulr ?bound_poly_accr_bound_gt0 //. by rewrite cauchymodP // !pmulr_rgt0 ?gtr0E ?bound_poly_accr_bound_gt0. rewrite -[p]swapXYK ![(swapXY (swapXY _)).[_, _]]horner2_swapXY. rewrite (le_lt_trans (@poly_accr_bound1P _ _ 0 (ubound x) _ _ _ _)) //; do ?by rewrite ?subr0 ?uboundP. apply: le_lt_trans (_ : `|x i - x j| * bound_poly_accr_bound y (swapXY p) 0 (ubound x) < _). by rewrite ler_wpmul2l ?normr_ge0 // bound_poly_accr_boundP. rewrite -ltr_pdivl_mulr ?bound_poly_accr_bound_gt0 //. by rewrite cauchymodP // !pmulr_rgt0 ?gtr0E ?bound_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)