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.)

[affeldt-aist]

Fixed by PR #1291

[affeldt-aist]

I have closed this issue by mistake (@Yosuke-Ito-345: thanks for noticing).

[Yosuke-Ito-345]

In the Section at_left_right in normedtype.v, the Variable R is assumed to be numFieldType.
Isn't it more rational to assume R to be realDomainType?
I think left and right have meanings only when the type is totally ordered.
I suggest this alternative because I would like to freely use the following lemma

ler_norm: forall [R : realDomainType] (x : R), x <= `|x|