fact: CoInductive Stream_eq_coind (s1 s2: ∞A) : Prop := stream_eq_coind : hd s1 = hd s2 → Stream_eq_coind (tl s1) (tl s2) → Stream_eq_coind s1 s2.
imports: MathClasses.theory.CoqStreams MathClasses.implementations.peano_naturals MathClasses.interfaces.abstract_algebra