opp_ ..., ... _opp -> oppr_ ..., ... _ oppr?

[IshiguroYoshihiro]

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.

analysis/theories/normedtype.v

Line 2399 in 99c3a83

Lemma opp_continuous : continuous (@GRing.opp V).

As there is also a oppe_continuous, I think that it is appropriate to name it as oppr_continuous.

analysis/theories/ereal.v

Lines 892 to 893 in 99c3a83

	Lemma oppe_continuous (R : realFieldType) :
	continuous (-%E : \bar R -> \bar R).

the followings are some of other,

analysis/classical/set_interval.v

Lines 453 to 454 in 99c3a83

	Lemma opp_itvoo (R : numDomainType) (x y : R) :
	-%R @` `]x, y[%classic = `](- y), (- x)[%classic.

analysis/theories/realfun.v

Lines 1960 to 1962 in 99c3a83

	Lemma variation_opp_rev a b f s : itv_partition a b s ->
	variation a b f s =
	variation (- b) (- a) (f \o -%R) (rev (belast (- a) (map -%R s))).