proposition: Lemma deriv_neq0_mono (p : {poly F}) (x : creal) : p^`().[x] != 0 -> { r : F & 0 < r & { i : nat & (cauchymod x r <= i)%N & (strong_mono p (x i) r)} }.
proof: Proof. move=> px_neq0. wlog : p px_neq0 / (0 < p^`().[x])%CR. case/neq_creal_ltVgt: (px_neq0)=> px_lt0; last exact. case/(_ (- p)). + pose_big_enough i. apply: (@neq_crealP (lbound px_neq0) i i); do ?by rewrite ?lbound_gt0. rewrite /= derivN hornerN subr0 normrN. by rewrite (lbound0_of px_neq0). by close. + pose_big_enough i. apply: (@lt_crealP (diff px_lt0) i i); do ?by rewrite ?diff_gt0. rewrite /= add0r derivN hornerN -subr_le0 opprK addrC. by rewrite (diff_of px_lt0) //. by close. move=> r r_ge0 [i hi]; move/strong_monoN; rewrite opprK=> sm. by exists r=> //; exists i. move=> px_gt0. pose b1 := poly_accr_bound p^`() 0 (1 + ubound x). pose b2 := poly_accr_bound2 p 0 (1 + ubound x). pose r : F := minr 1 (minr (diff px_gt0 / 4%:R / b1) (diff px_gt0 / 4%:R / b2 / 2%:R)). exists r. rewrite !lt_minr ?ltr01 ?pmulr_rgt0 ?gtr0E ?diff_gt0; by rewrite ?poly_accr_bound2_gt0 ?poly_accr_bound_gt0. pose_big_enough i. exists i => //; left; split; last first. move=> y hy; have := (@poly_accr_bound1P _ p^`() 0 (1 + ubound x) (x i) y). rewrite ?subr0 ler_paddl ?ler01 ?uboundP //. rewrite (le_trans (_ : _ <= r + `|x i|)) ?subr0; last 2 first. + rewrite (monoRL (addrNK _) (ler_add2r _)). by rewrite (le_trans (ler_sub_dist _ _)). + by rewrite ler_add ?le_minl ?lexx ?uboundP. move=> /(_ isT isT). rewrite ler_distl=> /andP[le_py ge_py]. rewrite (lt_le_trans _ le_py) // subr_gt0 -/b1. rewrite (lt_le_trans _ (diff0_of px_gt0)) //. apply: le_lt_trans (_ : r * b1 < _). by rewrite ler_wpmul2r ?poly_accr_bound_ge0. rewrite -ltr_pdivl_mulr ?poly_accr_bound_gt0 //. rewrite !lt_minl ltr_pmul2r ?invr_gt0 ?poly_accr_bound_gt0 //. by rewrite gtr_pmulr ?diff_gt0 // invf_lt1 ?gtr0E ?ltr1n ?orbT. exists (diff px_gt0 / 4%:R). by rewrite pmulr_rgt0 ?gtr0E ?diff_gt0. move=> y z neq_yz hy hz. have := (@poly_accr_bound1P _ p^`() 0 (1 + ubound x) (x i) z). have := @poly_accr_bound2P _ p 0 (1 + ubound x) z y; rewrite eq_sym !subr0. rewrite neq_yz ?ler01 ?ubound_ge0=> // /(_ isT). rewrite (le_trans (_ : _ <= r + `|x i|)); last 2 first. + rewrite (monoRL (addrNK _) (ler_add2r _)). by rewrite (le_trans (ler_sub_dist _ _)). + by rewrite ler_add ?le_minl ?lexx ?uboundP. rewrite (le_trans (_ : _ <= r + `|x i|)); last 2 first. + rewrite (monoRL (addrNK _) (ler_add2r _)). by rewrite (le_trans (ler_sub_dist _ _)). + by rewrite ler_add ?le_minl ?lexx ?uboundP. rewrite ler_paddl ?uboundP ?ler01 //. move=> /(_ isT isT); rewrite ler_distl=> /andP [haccr _]. move=> /(_ isT isT); rewrite ler_distl=> /andP [hp' _]. rewrite (lt_le_trans _ haccr) // (monoRL (addrK _) (ltr_add2r _)). rewrite (lt_le_trans _ hp') // (monoRL (addrK _) (ltr_add2r _)). rewrite (lt_le_trans _ (diff0_of px_gt0)) //. rewrite {2}[diff _](splitf 4) /= -!addrA ltr_add2l ltr_spaddl //. by rewrite pmulr_rgt0 ?gtr0E ?diff_gt0. rewrite -/b1 -/b2 ler_add //. + rewrite -ler_pdivl_mulr ?poly_accr_bound2_gt0 //. rewrite (le_trans (ler_dist_add (x i) _ _)) //. apply: le_trans (_ : r * 2%:R <= _). by rewrite mulrDr mulr1 ler_add // distrC. by rewrite -ler_pdivl_mulr ?ltr0n // !le_minl lexx !orbT. + rewrite -ler_pdivl_mulr ?poly_accr_bound_gt0 //. by rewrite (le_trans hz) // !le_minl lexx !orbT. 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)