proposition: Lemma EventuallyForAll_Str_nth_tl P n s : EventuallyForAll P s → EventuallyForAll P (Str_nth_tl n s).
proof: Proof. revert s. induction n. easy. intros. now apply IHn, EventuallyForAll_tl. Qed.
imports: MathClasses.theory.CoqStreams MathClasses.implementations.peano_naturals MathClasses.interfaces.abstract_algebra