proposition: Lemma rational_exp_neg_bounded_correct : forall (n:nat) (a:Q) (Ha : -1 <= a*(1#2)^n <= 0), (CRpower_2_iter n (rational_exp_small_neg Ha) == IRasCR (Exp (inj_Q IR a)))%CR.
proof: Proof. induction n. - intros. simpl. assert (-1 <= a <= 0) as Ha_simpl. { simpl in Ha. rewrite Qmult_1_r in Ha. exact Ha. } rewrite <- (rational_exp_small_neg_correct Ha_simpl). apply rational_exp_small_neg_wd. apply Qmult_1_r. - intros a Ha. simpl. rewrite -> compress_correct. rewrite <- rational_exp_neg_bounded_correct_aux. apply Cmap_wd. reflexivity. assert (-1 <= (a/2)*(1#2)^n <= 0) as Ha_div. { change (S n) with (1+n)%nat in Ha. rewrite Nat2Z.inj_add, Qpower_plus in Ha. simpl in Ha. rewrite Qmult_assoc in Ha. exact Ha. discriminate. } rewrite <- (IHn _ Ha_div). apply CRpower_2_iter_wd, rational_exp_small_neg_wd. unfold Qdiv. rewrite <- Qmult_assoc. apply Qmult_comp. reflexivity. change (/2) with ((1#2)^1). rewrite <- Qpower_plus. clear IHn. change 1%Z with (Z.of_nat 1). rewrite <- (Nat2Z.inj_add 1 n). reflexivity. discriminate. destruct Ha as [_ Ha]. apply (Qmult_le_r _ _ ((1#2)^S n)). apply Q.Qpower_0_lt. reflexivity. rewrite Qmult_0_l. exact Ha. 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