proposition: Lemma CRmorph_increasing_inv : forall {R1 R2 : ConstructiveReals} (f : ConstructiveRealsMorphism) (x y : CRcarrier R1), CRlt R2 (CRmorph f x) (CRmorph f y) -> CRlt R1 x y.
proof: Proof. intros. destruct (CR_Q_dense R2 _ _ H) as [q [H0 H1]]. destruct (CR_Q_dense R2 _ _ H0) as [r [H2 H3]]. apply lt_CR_of_Q, (CR_of_Q_lt R1) in H3. destruct (CRltLinear R1). destruct (s _ x _ H3). - exfalso. apply (CRmorph_increasing f) in c. destruct (CRmorph_rat f r) as [H4 _]. apply (CRle_lt_trans _ _ _ H4) in c. clear H4. exact (CRlt_asym _ _ c H2). - clear H2 H3 r. apply (CRlt_trans _ _ _ c). clear c. destruct (CR_Q_dense R2 _ _ H1) as [t [H2 H3]]. apply lt_CR_of_Q, (CR_of_Q_lt R1) in H2. destruct (s _ y _ H2). { exact c. } exfalso. apply (CRmorph_increasing f) in c. destruct (CRmorph_rat f t) as [_ H4]. apply (CRlt_le_trans _ _ _ c) in H4. clear c. exact (CRlt_asym _ _ H4 H3). Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs