proposition: Lemma CRlt_equiv : forall x y : CR, CRlt x y <-> exists n:nat, approximate x (Qpos2QposInf (1#Pos.of_nat n)) + (2#Pos.of_nat n) < approximate y (Qpos2QposInf (1#Pos.of_nat n)).
proof: Proof. split. - intros H. apply CR_lt_ltT in H. destruct H as [q H]. destruct q as [q qpos]; unfold proj1_sig in H. destruct q as [a b]. destruct a as [|a|a]. exfalso; inversion qpos. 2: exfalso; inversion qpos. clear qpos. assert (translate (1#b) x <= y)%CR. { rewrite (CRplus_le_r _ _ x) in H. ring_simplify in H. rewrite <- CRplus_translate. apply (@CRle_trans _ (' (Z.pos a # b) + x)%CR). 2: exact H. apply CRplus_le_r, CRle_Qle. change (b <= a*b)%positive. apply (Pos.le_trans _ (1*b)). apply Pos.le_refl. apply Pos.mul_le_mono_r. apply Pos.le_1_l. } clear H a. exists (Pos.to_nat (5*b)). rewrite Pos2Nat.id. apply (CRle_trans (lower_CRapproximation (translate (1#b) x) (1#5*b)%Qpos)) in H0. pose proof (upper_CRapproximation y (1#5*b)%Qpos) as H. apply (CRle_trans H0) in H. clear H0. apply CRle_Qle in H. simpl in H. rewrite Qplus_comm in H. unfold Qminus in H. rewrite <- Qplus_assoc in H. setoid_replace ((1 # b) + - (1 # b + b~0~0)) with ((3#5*b) + (1#5*b)) in H. rewrite Qplus_assoc in H. apply Qplus_le_l in H. refine (Qlt_le_trans _ _ _ _ H). apply Qplus_lt_r. apply Pos.mul_lt_mono_r. reflexivity. unfold canonical_names.equiv, stdlib_rationals.Q_eq. rewrite Qinv_plus_distr. setoid_replace (1#b) with (5#5*b) by reflexivity. rewrite Qinv_minus_distr. reflexivity. - intros [n H]. apply CR_lt_ltT. apply (@CRle_lt_trans _ _ _ (upper_CRapproximation x (1#Pos.of_nat n)%Qpos)). refine (CRlt_le_trans _ _ _ _ (lower_CRapproximation y (1#Pos.of_nat n)%Qpos)). apply CRlt_Qlt. simpl. apply (Qplus_lt_l _ _ (1# Pos.of_nat n)). ring_simplify. refine (Qle_lt_trans _ _ _ _ H). apply Qplus_le_r. apply Qle_refl. Qed.
imports: Coq.Reals.Abstract.ConstructiveReals CoRN.model.metric2.Qmetric CoRN.model.metric2.CRmetric CoRN.reals.fast.CRFieldOps CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.model.totalorder.QposMinMax Coq.Logic.ConstructiveEpsilon