proposition: Lemma littleo_lim0 (f : X -> Y) (h : _ -> Z) (x : X) : f @ x --> (0 : Y) -> [o_x f of h] x = 0.
proof: Proof. move/eqolim0P => ->; have [k /(_ _ [gt0 of 1 : R])/=] := littleo. by move=> /nbhs_singleton; rewrite mul1r normm_littleo normr_le0 => /eqP. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms