Comonad in Coq

I am interested in Coq.
We can use Coq for proving the satisfaction for the monad laws when we define the Monad-type structure.

I want to prove the comonad laws for stream comonad using Coq.
But it's so difficult for me... .