proposition: Lemma StopIndex_correct : forall x (e:AQ) (p r : positive), IsStopIndex x e p -> (forall q:positive, Pos.lt q p -> ~IsStopIndex x e q) -> Pos.le p r -> StopIndex x e r ≡ p.
proof: Proof. unfold IsStopIndex. intros. unfold StopIndex. destruct (iterate_stop_correct _ fS (fun y : positive and AQ and AQ => bool_decide_rel le (abs (fst (snd y))) (snd (snd y) * e0)) r (xH,x)) as [s [req [H8 H9]]]. rewrite req, fS_fst, Pos.pred_succ. clear req. destruct H9. - subst r. apply Pos.le_lteq in H7. destruct H7. 2: symmetry; exact H7. exfalso. specialize (H8 p H7). apply bool_decide_rel_false in H8. contradict H8. destruct (CRstreams.iterate _ fS p (1%positive, x)). exact H5. - destruct H9. apply bool_decide_rel_true in H10. clear H7 H9 r. destruct (Pos.lt_total s p). + exfalso. specialize (H6 s H7). contradict H6. destruct (CRstreams.iterate _ fS s (1%positive, x)). exact H10. + destruct H7. exact H7. exfalso. specialize (H8 p H7). apply bool_decide_rel_false in H8. contradict H8. destruct (CRstreams.iterate _ fS p (1%positive, x)). exact H5. Qed.
imports: Coq.QArith.Qabs CoRN.util.Qdlog CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric CoRN.model.reals.CRreal CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRstreams CoRN.reals.faster.ApproximateRationals CoRN.reals.faster.ARArith