proposition: Lemma iterate_stop_unique : forall (p q : positive) (x : X), stop (iterate p x) ≡ true -> stop (iterate q x) ≡ true -> (forall i:positive, Pos.lt i q -> stop (iterate i x) ≡ false) -> iterate_stop p x ≡ iterate q x.
proof: Proof. intros. pose proof (iterate_stop_correct p x) as [r [rpeq [H2 H3]]]. rewrite rpeq. replace r with q. reflexivity. destruct (Pos.lt_total q r). - exfalso. specialize (H2 q H4). rewrite H0 in H2. discriminate. - destruct H4. exact H4. exfalso. destruct H3. + subst r. specialize (H1 p H4). rewrite H in H1. discriminate. + destruct H3. specialize (H1 r H4). rewrite H1 in H5. discriminate. Qed.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric CoRN.metric2.Limit Coq.QArith.Qabs Coq.Arith.Arith Coq.QArith.Qpower CoRN.reals.fast.LazyNat Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.streams MathClasses.theory.series MathClasses.interfaces.abstract_algebra MathClasses.theory.streams