proposition: Lemma eq_some_oP (F : filter_on T) (e : T -> W) (f : T -> V) h : f = [o_F e of h] -> littleo_def F f e.
proof: Proof. by have := @eqadd_some_oP F f 0 e h; rewrite add0r subr0. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule