proposition: Lemma CRmorph_plus_rat : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x : CRcarrier R1) (q : Q), CRmorph f (CRplus R1 x (CR_of_Q R1 q)) == CRplus R2 (CRmorph f x) (CR_of_Q R2 q).
proof: Proof. split. - intro 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. apply (CRplus_lt_reg_r (CRopp R1 (CR_of_Q R1 q))). apply (CRlt_le_trans _ x). + apply (CRle_lt_trans _ (CR_of_Q R1 (r-q))). * apply (CRle_trans _ (CRplus R1 (CR_of_Q R1 r) (CR_of_Q R1 (-q)))). -- apply CRplus_le_compat_l. destruct (@CR_of_Q_opp R1 q). exact H. -- destruct (CR_of_Q_plus R1 r (-q)). exact H. * apply (CRmorph_increasing_inv f). apply (CRle_lt_trans _ (CR_of_Q R2 (r - q))). -- apply CRmorph_rat. -- apply (CRplus_lt_reg_r (CR_of_Q R2 q)). apply (CRle_lt_trans _ (CR_of_Q R2 r)). 2: exact H0. intro H. destruct (CR_of_Q_plus R2 (r-q) q) as [H1 _]. apply (CRlt_le_trans _ _ _ H) in H1. clear H. apply lt_CR_of_Q in H1. ring_simplify in H1. exact (Qlt_not_le _ _ H1 (Qle_refl _)). + destruct (CRisRing R1). apply (CRle_trans _ (CRplus R1 x (CRplus R1 (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))))). * apply (CRle_trans _ (CRplus R1 x 0)). -- destruct (CRplus_0_r x). exact H. -- apply CRplus_le_compat_l. destruct (Ropp_def (CR_of_Q R1 q)). exact H. * destruct (Radd_assoc x (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))). exact H1. - intro abs. destruct (CR_Q_dense R2 _ _ abs) as [r [H H0]]. clear abs. destruct (CRmorph_rat f r) as [_ H1]. apply (CRle_lt_trans _ _ _ H1) in H0. clear H1. apply CRmorph_increasing_inv in H0. apply (CRlt_asym _ _ H0). clear H0. apply (CRplus_lt_reg_r (CRopp R1 (CR_of_Q R1 q))). apply (CRle_lt_trans _ x). + destruct (CRisRing R1). apply (CRle_trans _ (CRplus R1 x (CRplus R1 (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))))). * destruct (Radd_assoc x (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))). exact H0. * apply (CRle_trans _ (CRplus R1 x 0)). -- apply CRplus_le_compat_l. destruct (Ropp_def (CR_of_Q R1 q)). exact H1. -- destruct (CRplus_0_r x). exact H1. + apply (CRlt_le_trans _ (CR_of_Q R1 (r-q))). * apply (CRmorph_increasing_inv f). apply (CRlt_le_trans _ (CR_of_Q R2 (r - q))). 2: apply CRmorph_rat. apply (CRplus_lt_reg_r (CR_of_Q R2 q)). apply (CRlt_le_trans _ _ _ H). apply (CRle_trans _ (CR_of_Q R2 (r-q+q))). -- intro abs. apply lt_CR_of_Q in abs. ring_simplify in abs. exact (Qlt_not_le _ _ abs (Qle_refl _)). -- destruct (CR_of_Q_plus R2 (r-q) q). exact H1. * apply (CRle_trans _ (CRplus R1 (CR_of_Q R1 r) (CR_of_Q R1 (-q)))). -- destruct (CR_of_Q_plus R1 r (-q)). exact H1. -- apply CRplus_le_compat_l. destruct (@CR_of_Q_opp R1 q). exact H1. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs