proposition: Lemma CRinv_Qinv : forall (x:Q) x_, CRinvT (inject_Q_CR x) x_ == inject_Q_CR (/x)%Q.
proof: Proof. intros x [[c x_]|[c x_]]; [change (' proj1_sig c <= 0 + - 'x)%CR in x_|change (' proj1_sig c <= ' x + - 0)%CR in x_]; unfold CRinvT; rewrite -> CRopp_Qopp, CRplus_Qplus, CRle_Qle in x_; try rewrite -> CRopp_Qopp; rewrite -> (@CRinv_pos_Qinv c). rewrite -> CRopp_Qopp. rewrite -> CReq_Qeq. assert (~x==0)%Q. intros H. rewrite -> H in x_. apply (Qle_not_lt _ _ x_). apply Qpos_ispos. field. intros X; apply H. assumption. rewrite -> Qplus_0_l in x_. assumption. reflexivity. rewrite -> Qplus_0_r in x_. assumption. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.metric2.Complete CoRN.metric2.ProductMetric CoRN.reals.fast.CRFieldOps CoRN.model.metric2.Qmetric CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders