One could define streams in the following manner

Section stream.
  Variable A : Type.

  CoInductive stream : Type :=
  | Cons : A -> stream -> stream.
End stream.

But as far as I can tell, such a coinductive stream is isomorphic to a function nat -> A. Arguably, working with the coinductive definition is harder.

What is an example of a situation where working with a coinductive type is a more intuitive option to express a certain object? When is it more convenient to use a coinductive proof? What are some instances when the coinductive proof/value makes the most sense?