proposition: Lemma CRmorph_abs : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x : CRcarrier R1), CRabs R2 (CRmorph f x) == CRmorph f (CRabs R1 x).
proof: Proof. assert (forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x : CRcarrier R1), CRabs R2 (CRmorph f x) <= CRmorph f (CRabs R1 x)). { intros. rewrite <- CRabs_def. split. - apply CRmorph_le. pose proof (CRabs_def _ x (CRabs R1 x)) as [_ H]. apply H, CRle_refl. - apply (CRle_trans _ (CRmorph f (CRopp R1 x))). + apply CRmorph_opp. + apply CRmorph_le. pose proof (CRabs_def _ x (CRabs R1 x)) as [_ H]. apply H, CRle_refl. } intros. split. 2: apply H. apply (CRmorph_le_inv (@SlowConstructiveRealsMorphism R2 R1)). apply (CRle_trans _ (CRabs R1 x)). - apply (Endomorph_id (CRmorph_compose f (@SlowConstructiveRealsMorphism R2 R1))). - apply (CRle_trans _ (CRabs R1 (CRmorph (@SlowConstructiveRealsMorphism R2 R1) (CRmorph f x)))). + apply CRabs_morph. apply CReq_sym, (Endomorph_id (CRmorph_compose f (@SlowConstructiveRealsMorphism R2 R1))). + apply H. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs