proposition: Lemma EventuallyForAll_tl P s : EventuallyForAll P s → EventuallyForAll P (tl s).
proof: Proof. repeat intro. now apply ForAll_tl. Qed.
imports: MathClasses.theory.CoqStreams MathClasses.implementations.peano_naturals MathClasses.interfaces.abstract_algebra