proposition: Lemma Str_alt_even_step : forall p x, Str_alt_decr x -> 0 <= Str_pth p x * Str_pth (p+2) x.
proof: Proof. intros. pose proof (H p). pose proof (H (Pos.succ p)). destruct H0, H1. replace (p+2)%positive with (Pos.succ (Pos.succ p)). destruct (Str_pth p x). destruct (Str_pth (Pos.succ p) x). destruct (Str_pth (Pos.succ (Pos.succ p)) x). unfold Qmult, Qle; simpl. rewrite Z.mul_1_r. unfold Qmult, Qle in H2; simpl in H2. rewrite Z.mul_1_r in H2. unfold Qmult, Qle in H3; simpl in H3. rewrite Z.mul_1_r in H3. destruct Qnum, Qnum1; try discriminate. destruct Qnum0. exfalso; apply H1; reflexivity. exfalso; apply H2; reflexivity. exfalso; apply H3; reflexivity. destruct Qnum0. exfalso; apply H1; reflexivity. exfalso; apply H3; reflexivity. exfalso; apply H2; reflexivity. rewrite <- Pos.add_1_r, <- Pos.add_1_r. rewrite <- 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