proposition: Lemma eqaddOE (F : filter_on T) (f g : T -> V) h (e : T -> W) : f = g + mkbigO a_tag F h e -> f = g +O_ F e.
proof: Proof. by move=> /eqadd_some_OP /eqaddOP. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule