proposition: Lemma neq_creal_horner p (x y : creal) : p.[x] != p.[y] -> x != y.
proof: Proof. move=> neq_px_py. pose d := lbound neq_px_py. pose_big_enough i. pose k := 2%:R + poly_accr_bound p (y i) d. have /andP[d_gt0 k_gt0] : (0 < d) && (0 < k). rewrite ?(ltr_spaddl, poly_accr_bound_ge0); by rewrite ?ltr0n ?ltW ?ltr01 ?lbound_gt0. pose_big_enough j. apply: (@neq_crealP (d / k) j j) => //. by rewrite ?(pmulr_lgt0, invr_gt0, ltr0n). rewrite ler_pdivr_mulr //. have /(_ j) // := (lbound_of neq_px_py). big_enough=> /(_ isT isT). apply: contraLR; rewrite -!ltNge=> hxy. rewrite (le_lt_trans (@poly_accr_bound1P _ _ (y i) d _ _ _ _)) //. + by rewrite ltW // cauchymodP. + rewrite ltW // (@split_dist_add (y j)) //; last first. by rewrite cauchymodP ?divrn_gt0. rewrite ltr_pdivl_mulr ?ltr0n // (le_lt_trans _ hxy) //. by rewrite ler_wpmul2l ?normr_ge0 // ler_paddr // poly_accr_bound_ge0. rewrite (le_lt_trans _ hxy) // ler_wpmul2l ?normr_ge0 //. by rewrite ler_paddl // ?ler0n. by close. 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)