proposition: Lemma Str_alt_zero : forall p x, Str_alt_decr x -> Str_pth p x == 0 -> Str_pth (Pos.succ p) x == 0.
proof: Proof. intros. pose proof (H p) as [H1 _]. rewrite H0 in H1. apply Qabs_Qle_condition in H1. destruct H1. apply (Qle_antisym _ _ H2) in H1. exact H1. 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