proposition: Lemma Str_alt_pos : forall p x, Str_alt_decr x -> 0 <= snd (f x) -> 0 <= snd (CRstreams.iterate (X * Q) f p~1 x).
proof: Proof. intros. rewrite Pos.xI_succ_xO. pose proof (Str_alt_neg p x H H0). specialize (H (p~0))%positive. unfold Str_pth in H. destruct H. destruct (Q_dec 0 (snd (CRstreams.iterate (X * Q) f p~0 x))). destruct s. exfalso; exact (Qlt_not_le _ _ q H1). apply Qopp_le_compat in H2. change (-0)%Q with 0%Q in H2. setoid_replace (- (snd (CRstreams.iterate (X * Q) f (Pos.succ p~0) x) * snd (CRstreams.iterate (X * Q) f p~0 x)))%Q with ( (snd (CRstreams.iterate (X * Q) f (Pos.succ p~0) x) * -snd (CRstreams.iterate (X * Q) f p~0 x)))%Q in H2 by (unfold equiv, Q_eq; ring). rewrite <- (Qmult_0_l (-snd (CRstreams.iterate (X * Q) f p~0 x))) in H2. apply Qmult_le_r in H2. exact H2. rewrite <- (Qplus_0_l (- snd (CRstreams.iterate (X * Q) f p~0 x))). rewrite <- Qlt_minus_iff. exact q. rewrite <- q in H. apply Qabs_Qle_condition in H. apply H. Qed.
imports: Coq.setoid_ring.ArithRing Coq.Bool.Bool Coq.QArith.Qpower Coq.QArith.Qabs CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRArith CoRN.model.metric2.Qmetric CoRN.reals.fast.LazyNat CoRN.reals.fast.CRstreams CoRN.metric2.Limit CoRN.model.totalorder.QposMinMax CoRN.classes.Qclasses MathClasses.interfaces.abstract_algebra