moving contents from `cantor.v` to `topology.v`

[affeldt-aist]

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.

@zstone1