Remove unicode from prove_real_assumsScript.sml

Prove the last unproved assumption for real package

Use HOL4's definitions of inv and / in the hol-real package

Because they are overspecified (in particular, defined for 0 as
divisor), they cannot be mapped directly to the underspecified
OpenTheory versions. However, we can prove they are equal to the
OpenTheory versions for all other inputs.

Start creating OpenTheory package for real

Attempting to build on the existing real numbers in OpenTheory base.
Hence the complication of prove_real_assums etc.

Currently, there are 2 axioms in the resulting package:

One is inv 0 = 0 which is unprovable for OpenTheory's inv, so will just
have to define our own inv (as with other underspecified constants).

The other is some complicated theorem that looks like the existence of a
supremum and which I have not figured out how to prove from what the
OpenTheory real package provides yet. (But it seems it should be
possible.)