proposition: Lemma rational_exp_neg_posH (q : Qpos) (n:nat) (a:Q) : -n ≤ a → a ≤ 0 → '(proj1_sig q) ≤ CRe_inv → '(proj1_sig q^n) ≤ IRasCR (Exp (inj_Q IR a)).
proof: Proof. intros Hn Ha small. rewrite <- IR_inj_Q_as_CR. rewrite <- IR_leEq_as_CR. stepl (inj_Q IR (proj1_sig q) [^]n) by (now (apply eq_symmetric; apply inj_Q_power)). assert (X:[0][<]inj_Q IR (`q)). stepl (inj_Q IR 0); [| now apply (inj_Q_nring IR 0)]. apply inj_Q_less. now destruct q. astepl (inj_Q IR (`q)[!](nring n)[//]X). unfold power. apply Exp_resp_leEq. destruct n. simpl (nring 0). rewrite cring_mult_zero_op. stepl (inj_Q IR 0); [| now apply (inj_Q_nring IR 0)]. apply inj_Q_leEq. assumption. apply (fun a b => (shift_mult_leEq' _ a b _ (nringS_ap_zero IR n))). apply nring_pos; auto with *. stepr (inj_Q IR (a/(S n))). apply Exp_cancel_leEq. astepl (inj_Q IR (`q)). rewrite -> IR_leEq_as_CR. rewrite -> IR_inj_Q_as_CR. assert (Ha0 : -(1)<=(a/S n)<=0). split. rewrite -> Qle_minus_iff. replace RHS with ((a + S n)*(1/(S n))) by (simpl; field;discriminate). replace LHS with (0*(1/(S n))) by simpl; ring. apply: mult_resp_leEq_rht;simpl. replace RHS with (a + - (- (P_of_succ_nat n))) by simpl; ring. rewrite <- Qle_minus_iff. assumption. rewrite <- (Qmake_Qdiv 1 (P_of_succ_nat n)). discriminate. replace RHS with (0*(1/(S n))) by simpl; ring. apply: mult_resp_leEq_rht;simpl. assumption. rewrite <- (Qmake_Qdiv 1 (P_of_succ_nat n)). discriminate. rewrite <- (rational_exp_small_neg_correct Ha0). apply CRle_trans with CRe_inv. apply small. unfold CRe_inv. do 2 rewrite -> (rational_exp_small_neg_correct). rewrite <- IR_leEq_as_CR. apply Exp_resp_leEq. apply inj_Q_leEq. tauto. assert (X0:inj_Q IR (inject_Z (S n))[#][0]). stepl (inj_Q IR (nring (S n))). stepl (@nring IR (S n)); [| now (apply eq_symmetric; apply (inj_Q_nring IR (S n)))]. apply (nringS_ap_zero). apply inj_Q_wd. apply nring_Q. stepl (inj_Q IR a[/]_[//]X0). apply div_wd. apply eq_reflexive. stepl (inj_Q IR (nring (S n))). apply inj_Q_nring. apply inj_Q_wd. apply nring_Q. apply eq_symmetric. apply inj_Q_div. 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