proposition: Lemma eqaddOP (F : filter_on T) (f g : T -> V) (e : T -> W) : (f = g +O_ F e) <-> (bigO_def F (f - g) e).
proof: Proof. by split=> [/eqadd_some_OP|fg_O_e]; rewrite ?bigOE // addrC addrNK. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule