https://github.com/math-comp/analysis/blob/1edbf7c822ab1a151c3f9574399f57d735d3c9f4/theories/normedtype_theory/normed_module.v#L1043 should be `r_`, TODO: check the whole script