proposition: Lemma funeposneg f : f = (fun x => f^\+ x - f^\- x).
proof: Proof. rewrite funeqE => x; rewrite /funepos /funeneg; have [|/ltW] := leP (f x) 0. by rewrite -{1}oppe0 -leeNr => /max_idPl ->; rewrite oppeK add0e. by rewrite -{1}oppe0 -leeNl => /max_idPr ->; rewrite sube0. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets fsbigop) mathcomp(functions cardinality set_interval) signed reals ereal topology normedtype sequences