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