proposition: Lemma bigO_bigO_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; have [k c1 kOg] := bigO _ g. have [k' c2 k'Ok] := bigO _ k. near=> c; move: k'Ok kOg; apply: filter_app2; near=> x => lek'c2k. rewrite -(@ler_pM2l _ c2%:num) // mulrA => /(le_trans lek'c2k) /le_trans. by apply; rewrite ler_pM//; near: c; exact: nbhs_pinfty_ge. 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