proposition: Lemma eqoO (F : filter_on T) (f : T -> V) (e : T -> W) : [o_F e of f] =O_F e.
proof: Proof. by apply/eqOP; exists 0; split => // k kgt0; apply: littleoP. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule