Multiplication of real numbers

[lowasser]

Work-in-progress, not ready for review, but at least putting this here to show how the parts fit together.

Will complete #1353 .

[lowasser]

(Has dependencies on #1336 and #1381 .)

[lowasser]

This PR now successfully defines the product of two reals and shows it is a real number. It doesn't show any properties whatsoever of the product of two reals -- no ring laws, no nothing -- but each of those may well be its own lift.

This is the hard one. Everything else should be comparatively easy.

There are a few drive-by changes I didn't end up needing thrown in, such as that the min in an opposite order is the max in the usual order and vice versa; I can pull those out into a separate thing or leave them in...

[lowasser]

Spent an hour thinking about how to prove the ring laws, and while I think all this work is correct and is going to show up in some form, I think the right way to prove all the ring laws and the like is to make rational intervals much more full featured, and show that they are...a semiring, actually, I think. That will probably allow this to be simplified, but not by much.

[lowasser]

Remarking as a draft; I want to submit #1497 first.

[lowasser]

I think this version qualifies as finally having proved all the basic properties of multiplication of real numbers, but it will obviously need breaking up -- possibly even further than the other active PRs (#1561, #1562, #1563).

[lowasser]

(Specifically, we have the ring laws, and we have that the standard embedding of rationals preserves multiplication.)