proposition: Lemma fposBfneg f x : fpos f x - fneg f x = f x.
proof: Proof. rewrite /fpos /fneg maxC. case: (leP (f x) 0); rewrite normr0 (subr0, sub0r) => ?. by rewrite ler0_norm ?opprK. by rewrite gtr0_norm. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology