https://github.com/math-comp/analysis/blob/c6942fdeb9dd7bcd94ae6ed80c3f74703d48f436/theories/normedtype_theory/normed_module.v#L1901 but this will cause generalization of other intermediate lemmas such as `bounded_near` this will be necessary to generalize the forthcoming Hahn-Banach theorem @mkerjean