proposition: Lemma CRmorph_one : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2), CRmorph f 1 == 1.
proof: Proof. intros. apply (CReq_trans _ (CRmorph f (CR_of_Q R1 1))). - apply CRmorph_proper. reflexivity. - apply CRmorph_rat. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs