proposition: Lemma CRtoAR_preserves_ltT : forall x y, prod (CRltT x y -> ARltT (cast CR AR x) (cast CR AR y)) (ARltT (cast CR AR x) (cast CR AR y) -> CRltT x y).
proof: Proof. intros x y. pose proof (CRAR_id x) as H6. pose proof (CRAR_id y) as H7. split. - intros. symmetry in H6. symmetry in H7. pose proof (CRltT_wd H6 H7 H5). apply ARtoCR_preserves_ltT in H8. exact H8. - intros H5. apply (CRltT_wd H6 H7). apply ARtoCR_preserves_ltT. exact 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