proposition: Lemma Cauchy_IR_inject_Q_as_CR_inject_Q : forall x:Q, (' x == Cauchy_IRasCR (Cauchy_CReals.inject_Q _ x))%CR.
proof: Proof. intros x. apply regFunEq_equiv, regFunEq_e. intros e. simpl. destruct (CS_seq_const Q_as_COrdField x (proj1_sig e) (Qpos_ispos e)). eapply ball_refl. apply (Qpos_nonneg (e + e)). 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