proposition: Lemma ARtoCR_preserves_invT x x_ x__: 'ARinvT x x_ = CRinvT ('x) x__.
proof: Proof. Proof with auto with qarith; try reflexivity. unfold ARinvT. destruct x_ as [Ec | Ec]. assert (CRltT ('x) 0) as Px. apply CRltT_wd with ('x) (cast AR CR 0). reflexivity. now apply rings.preserves_0. now apply ARtoCR_preserves_ltT. rewrite (CRinvT_irrelevant _ (inl Px)). unfold CRinvT. destruct Ec as [c Ec], Px as [d Ed]. autorewrite with ARtoCR. destruct (Qlt_le_dec (proj1_sig d) (proj1_sig ('c : Qpos))). rewrite (CRinv_pos_weaken d ('c))... change (cast Q CR (cast AQ Q (cast (AQ₊) AQ c)) ≤ -cast AR CR x). rewrite <-ARtoCR_inject, <-rings.preserves_negate. apply (order_preserving _). rewrite <-(rings.plus_0_l (-x))... rewrite (CRinv_pos_weaken ('c) d)... rewrite <-(rings.plus_0_l (-cast AR CR x))... assert (CRltT 0 ('x)) as Px. apply CRltT_wd with (cast AR CR 0) ('x). now apply rings.preserves_0. reflexivity. now apply ARtoCR_preserves_ltT. rewrite (CRinvT_irrelevant _ (inr Px)). unfold CRinvT. destruct Ec as [c Ec], Px as [d Ed]. autorewrite with ARtoCR. destruct (Qlt_le_dec (proj1_sig d) (proj1_sig ('c : Qpos))). rewrite (CRinv_pos_weaken d ('c))... change (cast Q CR (cast AQ Q (cast (AQ₊) AQ c)) ≤ cast AR CR x). rewrite <-ARtoCR_inject. apply (order_preserving _). setoid_replace x with (x - 0) by ring... rewrite (CRinv_pos_weaken ('c) d)... rewrite <-(rings.plus_0_r (cast AR CR x))... 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