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