proposition: Lemma rational_exp_neg_bounded_correct_aux (a : Q) : a ≤ 0 → (CRpower_N_bounded 2 (1 # 1)) (IRasCR (Exp (inj_Q IR (a / 2)))) = IRasCR (Exp (inj_Q IR a)).
proof: Proof. intros Ea. rewrite <- CRpower_N_bounded_correct. - change (CRpower_slow (IRasCR (Exp (inj_Q IR (a / 2)))) (N.to_nat 2))%CR with (IRasCR (Exp (inj_Q IR (a / 2))) * (IRasCR (Exp (inj_Q IR (a / 2))) * 1))%CR. rewrite CRmult_1_r. rewrite <- IR_mult_as_CR. apply IRasCR_wd. set (a':=inj_Q IR (a/2)). simpl. stepl (Exp (a'[+]a')); [| now apply Exp_plus]. apply Exp_wd. unfold a'. eapply eq_transitive. apply eq_symmetric; apply (inj_Q_plus IR). apply inj_Q_wd. change (a / (2#1) + a / (2#1) == a). field. - apply leEq_imp_AbsSmall. + rewrite <- IR_Zero_as_CR. apply IR_leEq_as_CR. apply less_leEq; apply Exp_pos. + apply (@CRle_trans _ (IRasCR [1])). apply IR_leEq_as_CR. apply Exp_leEq_One. stepr (inj_Q IR 0); [| now apply (inj_Q_nring IR 0)]. apply inj_Q_leEq. apply mult_cancel_leEq with (2:Q). constructor. change (a/2*2<=0). now replace LHS with a by (simpl; field; discriminate). simpl. rewrite IR_One_as_CR. apply CRle_refl. 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