proposition: Lemma NearBy_Infinity (s : Stream X) (x : X) : NearBy x QposInfinity s.
proof: Proof. Proof with trivial. unfold NearBy. simpl. revert s. cofix F. constructor... Qed.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax Coq.QArith.QArith Coq.Bool.Bool CoRN.metric2.Complete MathClasses.theory.CoqStreams MathClasses.interfaces.abstract_algebra MathClasses.theory.streams MathClasses.orders.naturals