proposition: Lemma iterate_stop_indep : forall (p q : positive) (x : X), stop (iterate p x) ≡ true -> stop (iterate q x) ≡ true -> iterate_stop p x ≡ iterate_stop q x.
proof: Proof. intros. pose proof (iterate_stop_correct p x) as [r [rpeq [H1 H2]]]. assert (stop (iterate r x) ≡ true) as rstop. { destruct H2. rewrite <- H2. exact H. apply H2. } rewrite rpeq. clear H2 rpeq H p. pose proof (iterate_stop_correct q x) as [s [sqeq [H H2]]]. assert (stop (iterate s x) ≡ true) as sstop. { destruct H2. rewrite <- H2. exact H0. apply H2. } rewrite sqeq. clear H2 sqeq H0 q. destruct (Pos.lt_total r s). - exfalso. specialize (H r H0). rewrite H in rstop. discriminate. - destruct H0. rewrite H0. reflexivity. exfalso. specialize (H1 s H0). rewrite H1 in sstop. 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