proposition: Lemma eqaddoEx (F : filter_on T) (f g : T -> V) h (e : T -> W) : (forall x, f x = g x + mklittleo a_tag F h e x) -> (forall x, f x = g x +o_(x \near F) (e x)).
proof: Proof. by have := @eqaddoE F f g h e; rewrite !funeqE. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule