proposition: Lemma stream_eq_Str_nth s1 s2 : s1 = s2 ↔ ∀ n, Str_nth n s1 = Str_nth n s2.
proof: Proof. split. intros E ?. now rewrite E. revert s1 s2. cofix FIX. intros s1 s2 E. constructor. now apply (E O). apply FIX. intros. now apply (E (S n)). Qed.
imports: MathClasses.theory.CoqStreams MathClasses.implementations.peano_naturals MathClasses.interfaces.abstract_algebra