proposition: Lemma rational_exp_small_neg_wd (a1 a2 : Q) (p1 : -(1) <= a1 <= 0) (p2 : -(1) <= a2 <= 0) : a1 == a2 → rational_exp_small_neg p1 = rational_exp_small_neg p2.
proof: Proof. intros E. unfold rational_exp_small_neg. rewrite <- CRplus_translate. rewrite <- CRplus_translate. apply CRplus_eq_r. apply AltSeries_wd. apply Pos.peano_ind. - unfold Str_pth; simpl. rewrite E. reflexivity. - intros. unfold Str_pth. rewrite iterate_succ, iterate_succ. simpl. unfold Str_pth in H. rewrite H. clear H. apply Qmult_comp. apply Qmult_comp. reflexivity. exact E. rewrite expStream_fst, expStream_fst. reflexivity. - 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