Added verified monads

This adds a typeclass of verified monads, which obey the monad laws in the same style as verified verified semigroups or monoids from Prelude.Algebra.
Here in `VerifiedApplicative` we verify `Functor` and `Applicative` to be compatible, so `map` is expressed via `<$>`. I suggest in `VerifiedMonad` we should also verify `Applicative` and `Monad` to be compatible, for `<$>` to be expressed via `>>=`. For example `mf <$> ma = do { f <- mf; a <- ma; return (f a) }`.