proposition: Lemma rational_exp_bound_power_2 : forall (a:Q), a <= 0 -> - inject_Z (2^Z.to_nat (Z.log2_up (Qceiling(-a)))) <= a.
proof: Proof. intros [[|n|n] d] Ha; simpl. discriminate. elim Ha. reflexivity. rewrite Z2Nat.id. clear Ha. rewrite <- (Qopp_involutive (Z.neg n # d)) at 2. apply Qopp_le_compat. change (-(Z.neg n#d)) with (Zpos n # d). apply Q.Zle_Qle_Qceiling. apply Z.log2_up_le_pow2. 2: apply Z.le_refl. apply Z2Nat.inj_lt. apply Z.le_refl. apply (Qceiling_resp_le 0). discriminate. apply Q.Qlt_lt_of_nat_inject_Z. reflexivity. apply Z.log2_up_nonneg. 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