proposition: Lemma eqoP (F : filter_on T) (e : T -> W) (f : T -> V) : (f =o_ F e) <-> (littleo_def F f e).
proof: Proof. by rewrite -[f]subr0 -eqaddoP -[f \- 0]/(f - 0) subr0 add0r. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule