moving contents from cantor.v to topology.v #1105
Description
NB: this is an issue that makes more sense with the HB version of MathComp-Analysis
Some contents of cantor.v can/should be moved to topology.v
such as lemma discrete_bool_compact or pointed_principal_filter/pointed_discrete_topology.
This is maybe better to this along with the splitting of topology.v.