proofs

[Richard]

I want to learn how to go about proving things like
    (p >>= j) >= k   ==   p >>= (\x->(j x >>= k))      
       where
          p >>= k  =  \s0 -> let (s1, a) = p s0
                             in k a s1

eg, verifying that the 3 monad laws hold for a specific monad.
also, verifying the more numerous laws every arrow should obey.

I could teach myself to do it clumsily, but I want to learn from others.
would learning category theory help me do this?  pointers to documents?
proof-assistant software?