proposition: Lemma rational_exp_pos_correct (a : Q) (Pa : 0 ≤ a) (c : Qpos) : ('proj1_sig c <= IRasCR (Exp (inj_Q IR (-a)%Q)))%CR → CRinv_pos c (IRasCR (Exp (inj_Q IR (-a)))) = IRasCR (Exp (inj_Q IR a)).
proof: Proof. intros Ec. assert (X: (IRasCR (Exp (inj_Q IR (-a)%Q)) >< 0)%CR). right. exists c. now ring_simplify. rewrite (CRinvT_pos_inv c X); trivial. rewrite <- IR_recip_as_CR_2. apply IRasCR_wd. apply eq_symmetric. eapply eq_transitive;[|apply div_wd; apply eq_reflexive]. apply Exp_inv'. rewrite (inj_Q_inv IR a), cg_inv_inv. 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