proposition: Lemma CR_inject_Q_as_Cauchy_IR_inject_Q : forall x:Q, Cauchy_CReals.inject_Q _ x [=] CRasCauchy_IR (' x)%CR.
proof: Proof. intros x. eapply Eq_alt_2_2. simpl. intros e He. exists 0. intros m Hm. unfold cg_minus. rstepr ([0]:Q). apply zero_AbsSmall. apply Qlt_le_weak. assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.reals.Cauchy_IR CoRN.tactics.CornTac Coq(Lia) CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.reals.fast.CRFieldOps