proposition: Lemma add_def_funeposneg f x : (f^\+ x +? - f^\- x).
proof: Proof. by rewrite /funeneg /funepos; case: (f x) => [r| |]; [rewrite -fine_max/=|rewrite /maxe /= ltNyr|rewrite /maxe /= ltNyr]. 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