proposition: Lemma inject_Q_AR_lt : ∀ q r : Q, q < r → ARltT (inject_Q_AR q) (inject_Q_AR r).
proof: Proof. intros. destruct (ARtoCR_preserves_ltT (' (' q)%CR) (' (' r)%CR)) as [_ a]. pose proof (inject_Q_AR_CR q). pose proof (inject_Q_AR_CR r). symmetry in H6. symmetry in H7. apply (ARltT_wd _ _ H6 _ _ H7). apply a. clear a H6 H7. pose proof (CRAR_id ('q)%CR). pose proof (CRAR_id ('r)%CR). symmetry in H6. symmetry in H7. apply (@CRltT_wd _ _ H6 _ _ H7). apply CRlt_Qlt, H5. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program Coq.setoid_ring.Ring Coq.QArith.Qabs CoRN.stdlib_omissions.Q MathClasses.misc.workaround_tactics CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.util.Qdlog CoRN.metric2.Complete CoRN.metric2.Prelength CoRN.model.metric2.Qmetric CoRN.metric2.MetricMorphisms CoRN.reals.fast.CRArith CoRN.reals.fast.CRpower MathClasses.implementations.stdlib_binary_naturals MathClasses.orders.minmax MathClasses.implementations.positive_semiring_elements CoRN.reals.faster.ApproximateRationals CoRN.reals.faster.AQmetric