proposition: Lemma RdisjunctEpsilon : forall a b c d : R, (a < b)%R \/ (c < d)%R -> (a < b)%R + (c < d)%R.
proof: Proof. intros. destruct (total_order_T a b). - destruct s. + left. exact r. + right. destruct H. * exfalso. subst a. exact (Rlt_asym b b H H). * exact H. - right. destruct H. + exfalso. exact (Rlt_asym _ _ H r). + exact H. Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms