proposition: Lemma Nearby_EventuallyForAll l ε s : EventuallyForAll (NearBy l ε) s.
proof: Proof. revert s. cofix FIX. constructor. now apply Nearby_tl. now apply (FIX (tl s)). Defined.
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