[yhbiwndu] Equality prover

Given two expressions defining real numbers, for example sqrt(2) and exp(log(2)/2), prove or disprove that they are equal.  If unequal, determine their ordering.

Proofs may fail, so the function may return many results:

data StrictOrdering = LT | GT;  -- hiding Prelude.Ordering
data EqualOrNot = Equal | Unequal (Maybe StrictOrdering);
data Answer = Maybe EqualOrNot;
(Haskell syntax)

This is a conceptually simple API.  The input expression syntax is unspecified.  Perhaps an additional Hint argument to guide the automated theorem prover.  For a successful proof, perhaps also return a proof object of unspecified type.

One inequality proof strategy is simply to calculate the values to a certain number if decimal places, paying attention to round off error.

Subroutine was wanted for the nerd clock.