Print proof of truthness

[coldfix]

For any expression EXPR that can be proven to be TRUE, it would be really nice to be able to obtain the proof for it, if interested. E.g. if an expression can be written as (or underestimated by) a linear combination of basic Shannon measures, print that linear combination.

This should be easy to accomplish by just printing the solution to the dual problem.

In the light of #4, I'd suggest something like dual I(X:Y) >= 0.