proposition: Lemma LazyExists_Str_nth_tl `{P : Stream A → Prop} `(ex : !LazyExists P s) (Ptl : EventuallyForAll P s) (n : nat) : LazyExists P (Str_nth_tl n s).
proof: Proof. induction n. easy. intros. simpl. rewrite <-tl_nth_tl. apply LazyExists_tl. now apply IHn. now apply ForAll_Str_nth_tl. 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