Should we make `not_near_at_rightP` an equivalence?

[Yosuke-Ito-345]

In the theory normedtype.v, we have the lemma not_near_at_rightP. The name contains the character P, but it states one-direct implication, not the equivalence. For me, this seems contradictory to the naming convention stated in https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md Should we add the other direction of not_near_at_rightP and make it an equivalence? (This is also the case with not_near_at_leftP.)