proposition: Lemma rational_exp_neg_posH' (c : Qpos) (a : Q) : a ≤ 0 → '(proj1_sig c) ≤ CRe_inv → '(proj1_sig (Qpos_power c (-Qfloor a))) ≤ IRasCR (Exp (inj_Q IR a)).
proof: Proof. intros Ha small. assert (X0:(0 <= -Qfloor a)%Z). apply Z.opp_nonneg_nonpos. rewrite Q.Zle_Qle. apply Qle_trans with a; [| assumption]. now apply Qfloor_le. setoid_replace (proj1_sig (Qpos_power c (-Qfloor a))) with (proj1_sig c ^ Z_to_nat X0). apply rational_exp_neg_posH; trivial. rewrite <- (Z_to_nat_correct X0). rewrite inject_Z_opp, Qopp_involutive. now apply Qfloor_le. now rewrite <- Z_to_nat_correct. 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