proposition: Lemma fune_abse f : abse \o f = f^\+ \+ f^\-.
proof: Proof. rewrite funeqE => x /=; have [fx0|/ltW fx0] := leP (f x) 0. - rewrite lee0_abs// /funepos /funeneg. move/max_idPr : (fx0) => ->; rewrite add0e. by move: fx0; rewrite -{1}oppe0 leeNr => /max_idPl ->. - rewrite gee0_abs// /funepos /funeneg; move/max_idPl : (fx0) => ->. by move: fx0; rewrite -{1}oppe0 leeNl => /max_idPr ->; rewrite adde0. 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