consider making the information `r > 0` explicit in `open_subball_rat`?

[affeldt-aist]

analysis/theories/normedtype_theory/normed_module.v

Line 2094 in 2e5e368

exists c r, let B : set R := ball (@ratr R c) (ratr r) in x \in B /\ B `<=` S.