I would like to prove in Haskell, whether in vanilla Haskell or using some libraries / tools, some simple theorems such as:

and [n*(n+1)/2 == sum [0..n] | n <- [0..]]

Is there a simple enough (ie. fully automated) way to prove such theorems in Haskell? I am not really interested in the proof itself, or a counterexample, but merely a yes/no answer.

There's this publication which doesn't seem practically usable; other than that most of everything else seems to be rather complex, ie. involving a completely separate language and not concerning Haskell.