proposition: Lemma CRmorph_plus : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x y : CRcarrier R1), CRmorph f (CRplus R1 x y) == CRplus R2 (CRmorph f x) (CRmorph f y).
proof: Proof. intros R1 R2 f. assert (forall (x y : CRcarrier R1), CRplus R2 (CRmorph f x) (CRmorph f y) <= CRmorph f (CRplus R1 x y)). { intros x y abs. destruct (CR_Q_dense R2 _ _ abs) as [r [H H0]]. clear abs. destruct (CRmorph_rat f r) as [H1 _]. apply (CRlt_le_trans _ _ _ H) in H1. clear H. apply CRmorph_increasing_inv in H1. apply (CRlt_asym _ _ H1). clear H1. destruct (CR_Q_dense R2 _ _ H0) as [q [H2 H3]]. apply lt_CR_of_Q in H2. assert (Qlt (r-q) 0) as epsNeg. { apply (Qplus_lt_r _ _ q). ring_simplify. exact H2. } destruct (CR_Q_dense R1 _ _ (CRplus_neg_rat_lt x (r-q) epsNeg)) as [s [H4 H5]]. apply (CRlt_trans _ (CRplus R1 (CR_of_Q R1 s) y)). 2: apply CRplus_lt_compat_r, H5. apply (CRmorph_increasing_inv f). apply (CRlt_le_trans _ (CRplus R2 (CR_of_Q R2 s) (CRmorph f y))). - apply (CRmorph_increasing f) in H4. destruct (CRmorph_plus_rat f x (r-q)) as [H _]. apply (CRle_lt_trans _ _ _ H) in H4. clear H. destruct (CRmorph_rat f s) as [_ H1]. apply (CRlt_le_trans _ _ _ H4) in H1. clear H4. apply (CRlt_trans _ (CRplus R2 (CRplus R2 (CRmorph f x) (CR_of_Q R2 (r - q))) (CRmorph f y))). 2: apply CRplus_lt_compat_r, H1. apply (CRlt_le_trans _ (CRplus R2 (CRplus R2 (CR_of_Q R2 (r - q)) (CRmorph f x)) (CRmorph f y))). + apply (CRlt_le_trans _ (CRplus R2 (CR_of_Q R2 (r - q)) (CRplus R2 (CRmorph f x) (CRmorph f y)))). * apply (CRle_lt_trans _ (CRplus R2 (CR_of_Q R2 (r - q)) (CR_of_Q R2 q))). 2: apply CRplus_lt_compat_l, H3. intro abs. destruct (CR_of_Q_plus R2 (r-q) q) as [_ H4]. apply (CRle_lt_trans _ _ _ H4) in abs. clear H4. destruct (CRmorph_rat f r) as [_ H4]. apply (CRlt_le_trans _ _ _ abs) in H4. clear abs. apply lt_CR_of_Q in H4. ring_simplify in H4. exact (Qlt_not_le _ _ H4 (Qle_refl _)). * destruct (CRisRing R2); apply Radd_assoc. + apply CRplus_le_compat_r. destruct (CRisRing R2). destruct (Radd_comm (CRmorph f x) (CR_of_Q R2 (r - q))). exact H. - intro abs. destruct (CRmorph_plus_rat f y s) as [H _]. apply H. clear H. apply (CRlt_le_trans _ (CRplus R2 (CR_of_Q R2 s) (CRmorph f y))). + apply (CRle_lt_trans _ (CRmorph f (CRplus R1 (CR_of_Q R1 s) y))). * apply CRmorph_proper. destruct (CRisRing R1); apply Radd_comm. * exact abs. + destruct (CRisRing R2); apply Radd_comm. } split. - apply H. - specialize (H (CRplus R1 x y) (CRopp R1 y)). intro abs. apply H. clear H. apply (CRle_lt_trans _ (CRmorph f x)). + apply CRmorph_proper. destruct (CRisRing R1). apply (CReq_trans _ (CRplus R1 x (CRplus R1 y (CRopp R1 y)))). * apply CReq_sym, Radd_assoc. * apply (CReq_trans _ (CRplus R1 x 0)). 2: apply CRplus_0_r. destruct (CRisRingExt R1). apply Radd_ext. -- apply CReq_refl. -- apply Ropp_def. + apply (CRplus_lt_reg_r (CRmorph f y)). apply (CRlt_le_trans _ _ _ abs). clear abs. apply (CRle_trans _ (CRplus R2 (CRmorph f (CRplus R1 x y)) 0)). * destruct (CRplus_0_r (CRmorph f (CRplus R1 x y))). exact H. * apply (CRle_trans _ (CRplus R2 (CRmorph f (CRplus R1 x y)) (CRplus R2 (CRmorph f (CRopp R1 y)) (CRmorph f y)))). -- apply CRplus_le_compat_l. apply (CRle_trans _ (CRplus R2 (CRopp R2 (CRmorph f y)) (CRmorph f y))). ++ destruct (CRplus_opp_l (CRmorph f y)). exact H. ++ apply CRplus_le_compat_r. destruct (CRmorph_opp f y). exact H. -- destruct (CRisRing R2). destruct (Radd_assoc (CRmorph f (CRplus R1 x y)) (CRmorph f (CRopp R1 y)) (CRmorph f y)). exact H0. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs