reals are unique

Stream: Is there code for X?

[Kevin Buzzard]

Did we ever get one or both of "two complete totally ordered archimedean fields are equiv" or "a complete totally ordered archimedean field is equiv to \R"?

[Bryan Gin-ge Chen]

I think this is in #3292 by @Alex J. Best.

[Alex J. Best]

Johan left me some great comments, but I haven't had much lean time to implement them yet

[Alex J. Best]

If anyone wants to make any changes feel free to do so by the way, I just haven't had the chance to myself and really don't have a strong opinion RE: naming and what files things should go in.