proposition: Lemma CRlt_or_epsilon : (forall a b c d : CR, CRlt a b \/ CRlt c d -> (a < b)%CR + (c < d)%CR).
proof: Proof. intros. assert (exists n:nat, approximate a (Qpos2QposInf (1#Pos.of_nat n)) + (2#Pos.of_nat n) < approximate b (Qpos2QposInf (1#Pos.of_nat n)) \/ approximate c (Qpos2QposInf (1#Pos.of_nat n)) + (2#Pos.of_nat n) < approximate d (Qpos2QposInf (1#Pos.of_nat n))). { destruct H. - apply CRlt_equiv in H. destruct H as [n H]. exists n. left. exact H. - apply CRlt_equiv in H. destruct H as [n H]. exists n. right. exact H. } apply constructive_indefinite_ground_description_nat in H0. - destruct H0 as [n H0]. destruct (Qlt_le_dec (approximate a (Qpos2QposInf (1 # Pos.of_nat n)) + (2 # Pos.of_nat n)) (approximate b (Qpos2QposInf (1 # Pos.of_nat n)))). + left. apply CR_lt_ltT, CRlt_equiv. exists n. exact q. + right. apply CR_lt_ltT, CRlt_equiv. exists n. destruct H0. 2: exact H0. exfalso. exact (Qlt_not_le _ _ H0 q). - intro n. clear H0 H. destruct (Qlt_le_dec (approximate a (Qpos2QposInf (1 # Pos.of_nat n)) + (2 # Pos.of_nat n)) (approximate b (Qpos2QposInf (1 # Pos.of_nat n)))). left. left. exact q. destruct (Qlt_le_dec (approximate c (Qpos2QposInf (1 # Pos.of_nat n)) + (2 # Pos.of_nat n)) (approximate d (Qpos2QposInf (1 # Pos.of_nat n)))). left. right. exact q0. right. intros [H|H]. exact (Qlt_not_le _ _ H q). exact (Qlt_not_le _ _ H q0). 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