proposition: Lemma CRmorph_opp : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x : CRcarrier R1), CRmorph f (- x) == - CRmorph f x.
proof: Proof. split. - intro abs. destruct (CR_Q_dense R2 _ _ abs) as [q [H H0]]. clear abs. destruct (CRmorph_rat f q) as [H1 _]. apply (CRlt_le_trans _ _ _ H) in H1. clear H. apply CRmorph_increasing_inv in H1. apply CRopp_gt_lt_contravar in H0. destruct (@CR_of_Q_opp R2 q) as [H2 _]. apply (CRlt_le_trans _ _ _ H0) in H2. clear H0. pose proof (CRopp_involutive (CRmorph f x)) as [H _]. apply (CRle_lt_trans _ _ _ H) in H2. clear H. destruct (CRmorph_rat f (-q)) as [H _]. apply (CRlt_le_trans _ _ _ H2) in H. clear H2. apply CRmorph_increasing_inv in H. destruct (@CR_of_Q_opp R1 q) as [_ H2]. apply (CRlt_le_trans _ _ _ H) in H2. clear H. apply CRopp_gt_lt_contravar in H2. pose proof (CRopp_involutive (CR_of_Q R1 q)) as [H _]. apply (CRle_lt_trans _ _ _ H) in H2. clear H. exact (CRlt_asym _ _ H1 H2). - intro abs. destruct (CR_Q_dense R2 _ _ abs) as [q [H H0]]. clear abs. destruct (CRmorph_rat f q) as [_ H1]. apply (CRle_lt_trans _ _ _ H1) in H0. clear H1. apply CRmorph_increasing_inv in H0. apply CRopp_gt_lt_contravar in H. pose proof (CRopp_involutive (CRmorph f x)) as [_ H1]. apply (CRlt_le_trans _ _ _ H) in H1. clear H. destruct (@CR_of_Q_opp R2 q) as [_ H2]. apply (CRle_lt_trans _ _ _ H2) in H1. clear H2. destruct (CRmorph_rat f (-q)) as [_ H]. apply (CRle_lt_trans _ _ _ H) in H1. clear H. apply CRmorph_increasing_inv in H1. destruct (@CR_of_Q_opp R1 q) as [H2 _]. apply (CRle_lt_trans _ _ _ H2) in H1. clear H2. apply CRopp_gt_lt_contravar in H1. pose proof (CRopp_involutive (CR_of_Q R1 q)) as [_ H]. apply (CRlt_le_trans _ _ _ H1) in H. clear H1. exact (CRlt_asym _ _ H0 H). Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs