{l} : IsLimit _ _ xs l -> locator l. Proof. intros islim. intros q r ltqr. set (epsilon := (Qpos_diff q r ltqr) / 3). assert (ltqepsreps : q + ' epsilon < r - ' epsilon). { apply (strictly_order_reflecting (+'epsilon)). rewrite <- (plus_assoc r (-'epsilon) ('epsilon)). rewrite plus_negate_l. rewrite plus_0_r. rewrite <- (plus_assoc q ('epsilon) ('epsilon)). apply (strictly_order_reflecting ((-q)+)). rewrite (plus_assoc (-q) q _). rewrite plus_negate_l, plus_0_l. rewrite (plus_comm (-q) r). rewrite <- (mult_1_r ('epsilon)). rewrite <- plus_mult_distr_l. unfold epsilon, cast, Qpos_diff; cbn. rewrite <- (mult_assoc (r-q) (/3) 2). pattern (r-q) at 2. rewrite <- (mult_1_r (r-q)). assert (rqpos : 0 < r-q) by apply (Qpos_diff q r ltqr). apply (strictly_order_preserving ((r-q)*.)). apply (strictly_order_reflecting (3*.)). rewrite (mult_assoc 3 (/3) 2). rewrite (dec_recip_inverse 3). - rewrite mult_1_r, mult_1_l. exact lt_2_3. - apply apart_ne, positive_apart_zero, lt_0_3. } destruct (ls (M (epsilon / 2)) (q + ' epsilon) (r - ' epsilon) ltqepsreps) as [ltqepsxs|ltxsreps]. + apply inl. rewrite preserves_plus in ltqepsxs. assert (ltqxseps : ' q < xs (M (epsilon / 2)) - ' (' epsilon)) by (apply flip_lt_minus_r; assumption). refine (transitivity ltqxseps _). apply (modulus_close_limit _ _ _ _ _). + apply inr. rewrite (preserves_plus r (-'epsilon)) in ltxsreps. rewrite (preserves_negate ('epsilon)) in ltxsreps. assert (ltxsepsr : xs (M (epsilon / 2)) + ' (' epsilon) < ' r) by (apply flip_lt_minus_r; assumption). refine (transitivity _ ltxsepsr). apply (modulus_close_limit _ _ _ _ _). Qed.
Require Import