proposition: Lemma funeD_posD f g : f \+ g = (f^\+ \+ g^\+) \- (f^\- \+ g^\-).
proof: Proof. apply/funext => x; rewrite /funepos /funeneg. have [|fx0] := leP 0 (f x); last rewrite add0e. - rewrite -{1}oppe0 leeNl => /max_idPr ->; have [|/ltW] := leP 0 (g x). by rewrite -{1}oppe0 leeNl => /max_idPr ->; rewrite adde0 sube0. by rewrite -{1}oppe0 -leeNr => /max_idPl ->; rewrite adde0 sub0e oppeK. - move/ltW : (fx0); rewrite -{1}oppe0 leeNr => /max_idPl ->. have [|] := leP 0 (g x); last rewrite add0e. by rewrite -{1}oppe0 leeNl => /max_idPr ->; rewrite adde0 oppeK addeC. move gg' : (g x) => g'; move: g' gg' => [g' gg' g'0|//|goo _]. + move/ltW : (g'0); rewrite -{1}oppe0 -leeNr => /max_idPl => ->. by rewrite fin_num_oppeD// 2!oppeK. + by rewrite /maxe /=; case: (f x) fx0. 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