proposition: Lemma Str_alt_neg : forall p x, Str_alt_decr x -> 0 <= snd (f x) -> Str_pth (p~0) x <= 0.
proof: Proof. apply (Pos.peano_ind (fun p => forall (x : X * Q), Str_alt_decr x → 0 <= snd (f x) → Str_pth (p~0) x <= 0)). - intros. simpl. specialize (H xH). unfold Str_pth in H. simpl in H. destruct H. destruct (Q_dec (snd (f x)) 0). destruct s. exfalso; exact (Qlt_not_le _ _ q H0). rewrite <- (Qmult_0_l (snd (f x))) in H1. apply Qmult_le_r in H1. exact H1. exact q. rewrite q in H. exact (Qle_trans _ _ _ (Qle_Qabs _) H). - intros. pose proof (Str_alt_even_step (p~0) x H0). specialize (H x H0 H1). replace (p~0+2)%positive with ((Pos.succ p)~0)%positive in H2. apply Qnot_lt_le. intro abs. rewrite <- (Qmult_0_l (Str_pth ((Pos.succ p)~0) x)) in H2. apply Qmult_le_r in H2. 2: exact abs. apply (Qle_antisym _ _ H) in H2. clear H. apply (Str_alt_zero _ _ H0) in H2. apply (Str_alt_zero _ _ H0) in H2. rewrite <- Pos.double_succ in H2. rewrite H2 in abs. exact (Qlt_irrefl 0 abs). rewrite Pos.double_succ. rewrite <- Pos.add_1_r, <- Pos.add_1_r, <- Pos.add_assoc. reflexivity. 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