Theorem nhds_eq_real

feat(analysis/real): swap out the definition of real, shorten proofs

feat(topology): restructure order topologies; (start) proof that ennreal is a topological monoid