proposition: Lemma eqolim0P (F : filter_on T) (f : T -> V) : f @ F --> (0 : V) <-> f =o_F (cst (1 : K^o)).
proof: Proof. by rewrite eqolimP add0r -[f \- cst 0]/(f - 0) subr0. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule