proposition: Lemma Str_nth_tl_S (s : ∞A) n : Str_nth_tl (S n) s ≡ tl (Str_nth_tl n s).
proof: Proof. now rewrite tl_nth_tl. Qed.
imports: MathClasses.theory.CoqStreams MathClasses.implementations.peano_naturals MathClasses.interfaces.abstract_algebra