proposition: Lemma expStream_alt : -1 <= a <= 0 -> Str_alt_decr _ expStream (xH,1).
proof: Proof. intros aneg p. unfold Str_pth. rewrite iterate_succ. generalize (iterate (positive and Q) expStream p (1%positive, 1)). intros [n q]. unfold expStream, snd, fst. split. - rewrite <- Qmult_assoc. rewrite <- (Qmult_1_l (Qabs q)). rewrite Qabs_Qmult, Qmult_comm. apply Qmult_le_compat_r. 2: apply Qabs_nonneg. rewrite Qabs_Qmult. apply (Qle_trans _ (1 * Qabs (1#n))). apply Qmult_le_compat_r. 2: apply Qabs_nonneg. apply Qabs_Qle_condition. split. apply aneg. apply (Qle_trans _ 0). apply aneg. discriminate. rewrite Qmult_1_l. apply Pos.le_1_l. - destruct aneg as [_ aneg]. rewrite <- (Qmult_comm a). rewrite <- Qmult_assoc, <- Qmult_assoc. rewrite <- (Qmult_0_l (q * ((1 # n) * q))). apply Qmult_le_compat_r. exact aneg. rewrite Qmult_comm. destruct q, Qnum; unfold Qle; discriminate. 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