proposition: Lemma Qinv_le_compat : forall (a b : Q), 0 < a -> a <= b -> /b <= /a.
proof: Proof. intros. apply Qle_shift_inv_l. exact H. apply (Qmult_le_l _ _ b). exact (Qlt_le_trans _ a _ H H0). rewrite Qmult_1_r, Qmult_assoc. rewrite Qmult_inv_r. rewrite Qmult_1_l. exact H0. intro abs. rewrite abs in H0. apply (Qlt_irrefl 0). exact (Qlt_le_trans _ _ _ H H0). Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRAlternatingSum_alg CoRN.reals.fast.CRstreams CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.iso_CReals Coq.QArith.Qpower CoRN.algebra.COrdFields2 CoRN.model.ordfields.Qordfield CoRN.transc.PowerSeries CoRN.reals.fast.CRpower CoRN.transc.Exponential CoRN.transc.RealPowers CoRN.reals.fast.Compress Coq.NArith.Ndigits CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.reals.fast.CRsign CoRN.reals.Q_in_CReals Coq.QArith.Qabs Coq.QArith.Qround CoRN.tactics.CornTac MathClasses.theory.int_pow MathClasses.interfaces.abstract_algebra