`funrpos` and `funepos` should be factorized

[affeldt-aist]

as observed by @t6s in the following comment:

#1865 (comment)

[t6s]

porderedNmodType is in mathcomp, but that's not enough. we will need a bit more structure

[affeldt-aist]

We can maybe define:

Section funposneg.
Context {T : Type} {R : porderZmodType}.

Definition funpos (f : T -> R) := fun x => Num.max (f x) 0.
Definition funneg (f : T -> R) := fun x => Num.max (- f x) 0.

End funposneg.

and once numZmodType is available do:

Section funposneg_lemmas.
Context {T : Type} {R : numZmodType}.
Implicit Types (f g : T -> R).

Local Notation "f ^\+" := (funpos f).
Local Notation "f ^\-" := (funneg f).

Lemma funpos_ge0 f x : 0 <= f^\+ x.

...