proposition: Lemma rational_exp_correct (a : Q) : (rational_exp a = IRasCR (Exp (inj_Q IR a)))%CR.
proof: Proof. unfold rational_exp. destruct a as [[|n|n] d]. - rewrite <- IR_One_as_CR. apply IRasCR_wd. setoid_replace (inj_Q IR (0 # d)) with (cm_unit IR). symmetry. apply Exp_zero. rewrite <- inj_Q_Zero. apply inj_Q_wd. reflexivity. - rewrite rational_exp_neg_correct. apply (@rational_exp_pos_correct (Zpos n#d)). discriminate. apply (rational_exp_neg_posH' (1#3)). discriminate. now apply CRe_inv_posH. - apply rational_exp_neg_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