See [this line](https://github.com/math-comp/analysis/blob/3edd010fa7b101f449c6f364e0dfacb51b546496/theories/cauchyetoile.v#L196), for topological zmodtype.