math-comp
`opp_ ...`, `... _opp` -> `oppr_ ...`, `... _ oppr`?
I found some lemmas about GRing.opp which is named opp_ ... or ... _opp, not oppr_ ... or ... _oppr.
I suppose these may be for distinguish between GRing.opp for number and for function, but it bothers me a little.
For instance, opp_continuous in normedtype.v.
https://github.com/math-comp/analysis/blob/99c3a8336d2ca461f2766d18293cd26cbe4b1069/theories/normedtype.v#L2399
As there is also a oppe_continuous, I think that it is appropriate to name it as oppr_continuous.
https://github.com/math-comp/analysis/blob/99c3a8336d2ca461f2766d18293cd26cbe4b1069/theories/ereal.v#L892-L893
the followings are some of other, https://github.com/math-comp/analysis/blob/99c3a8336d2ca461f2766d18293cd26cbe4b1069/classical/set_interval.v#L453-L454 https://github.com/math-comp/analysis/blob/99c3a8336d2ca461f2766d18293cd26cbe4b1069/theories/realfun.v#L1960-L1962
