proposition: Lemma inject_Q_strext : @fun_strext _ CRasCSetoid inject_Q_CR.
proof: Proof. intros x y [Hxy|Hxy]. apply: Qlt_not_eq. apply Qnot_le_lt. intros H. absurd ('y <= 'x). rewrite -> leEq_def. auto with *. rewrite -> CRle_Qle. auto. apply ap_symmetric. apply: Qlt_not_eq. apply Qnot_le_lt. intros H. absurd ('x <= 'y). rewrite -> leEq_def. auto with *. rewrite -> CRle_Qle. auto. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.model.reals.CRreal CoRN.metric2.Complete CoRN.reals.fast.CRFieldOps CoRN.model.rings.Qring CoRN.algebra.CRing_Homomorphisms CoRN.model.metric2.Qmetric CoRN.tactics.CornTac CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders CRArith