proposition: Lemma StopIndex_stop_fuel : forall x (e:AQ) (candidate : positive), (forall p:positive, Pos.lt p candidate -> ~IsStopIndex x e p) -> StopIndex x e candidate ≡ candidate.
proof: Proof. 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)) candidate (xH,x)) as [r [req [H6 H7]]]. rewrite req, fS_fst, Pos.pred_succ. clear req. destruct H7. symmetry. exact H7. destruct H7. exfalso. clear H6. specialize (H5 r H7). apply bool_decide_rel_true in H8. contradict H5. unfold IsStopIndex. destruct (CRstreams.iterate _ fS r (1%positive, x)). exact H8. 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