proposition: Lemma rational_exp_small_neg_correct : forall (a:Q) Ha, (@rational_exp_small_neg a Ha == IRasCR (Exp (inj_Q IR a)))%CR.
proof: Proof. intros a Ha. unfold rational_exp_small_neg. rewrite <- CRplus_translate. setoid_replace 1%CR with (IRasCR ((λ n : nat, Exp_ps n (inj_Q IR a) (fun_series_inc_IR realline Exp_ps Exp_conv (inj_Q IR a) I n)) 0%nat)). apply: AltSeries_correct. intro p. apply exp_ps_correct. simpl. rewrite <- IR_One_as_CR. apply IRasCR_wd. rewrite mult_one. unfold cf_div. rewrite one_mult. rewrite <- inv_one at 1. apply f_rcpcl_wd. rewrite cm_lft_unit. reflexivity. 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