proposition: Lemma ARtoCR_preserves_apartT_0 x : prod (ARapartT x 0 -> CRapartT ('x) 0) (CRapartT ('x) 0 -> ARapartT x 0).
proof: Proof. split; intros. - apply (@CRapartT_wd ('x)%mc _ (reflexivity _) (cast AR CR 0)). apply ARtoCR_preserves_0. apply ARtoCR_preserves_apartT, X. - apply (@CRapartT_wd ('x)%mc _ (reflexivity _) _ (cast AR CR 0)) in H5. apply ARtoCR_preserves_apartT in H5. exact H5. symmetry; apply ARtoCR_preserves_0. Defined.
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