proposition: Lemma ARinv_0_lt_compat : ∀ (r : AR) (rnz : (ARltS r (inject_Q_AR 0) + ARltS (inject_Q_AR 0) r)%type), ARltS (inject_Q_AR 0) r → ARltS (inject_Q_AR 0) (ARinvS r rnz).
proof: Proof. intros r rnz H5. destruct (ARtoCR_preserves_ltT (inject_Q_AR 0) (ARinvS r rnz)) as [_ a]. apply a. clear a. assert (0 = ARtoCR (inject_Q_AR 0))%CR as H7. { rewrite <- (CRAR_id 0%CR). unfold cast. rewrite (inject_Q_AR_CR 0). reflexivity. } pose proof (ARtoCR_preserves_apartT_0 r ) as [ap _]. pose proof (ARtoCR_preserves_invT r (ARapartT_wd r r (inject_Q_AR 0) (' zero0) (reflexivity r) AR_zero rnz) (ap (ARapartT_wd r r (inject_Q_AR 0) (' zero0) (reflexivity r) AR_zero rnz))) as H6. symmetry in H6. apply (CRltT_wd H7 H6). clear H6. apply CRinv_0_lt_compat. destruct (ARtoCR_preserves_ltT (inject_Q_AR 0) r) as [a _]. apply a in H5. clear a. symmetry in H7. apply (CRltT_wd H7 (reflexivity _)). exact H5. Qed.
imports: Coq.Reals.Abstract.ConstructiveReals CoRN.reals.faster.ARArith CoRN.reals.faster.ARabs CoRN.metric2.Metric CoRN.metric2.Complete CoRN.metric2.MetricMorphisms CoRN.model.metric2.Qmetric CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs ConstructiveFastReals