It would be nice to have a file for topologies on the real line and the Euclidean planes, like "real_topology.v". (comment by @t6s in the conversion about PR #677 )
