proposition: Lemma bigO (F : filter_on T) (g : T -> W) (f : {O_F g}) : bigO_spec F g f.
proof: Proof. by have /bigO_exP [_/posnumP[k] kP] := bigOP f; exists k. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule