proposition: Lemma bigO_littleo_eqo {F : filter_on T} (g : T -> W) (f : T -> V) (h : T -> X) : f =o_F g -> [O_F f of h] =o_F g.
proof: Proof. move->; apply/eqoP => _/posnumP[e]; have [k c] := bigO. apply: filter_app; near=> x => /le_trans; apply. by rewrite -ler_pdivlMl // mulrA; near: x; apply: littleoP. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule