proposition: Lemma funeD_Dpos f g : f \+ g = (f \+ g)^\+ \- (f \+ g)^\-.
proof: Proof. apply/funext => x; rewrite /funepos /funeneg; have [|/ltW] := leP 0 (f x + g x). - by rewrite -{1}oppe0 -leeNl => /max_idPr ->; rewrite sube0. - by rewrite -{1}oppe0 -leeNr => /max_idPl ->; rewrite oppeK add0e. 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