proposition: Lemma ae_eq_funeposneg f g : ae_eq f g <-> ae_eq f^\+ g^\+ /\ ae_eq f^\- g^\-.
proof: Proof. split=> [fg|[]]. by rewrite /funepos /funeneg; split; apply: filterS fg => x /[apply] ->. apply: filterS2 => x + + Dx => /(_ Dx) fg /(_ Dx) gf. by rewrite (funeposneg f) (funeposneg g) fg gf. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)