proposition: Lemma opp_bigO_subproof (F : filter_on T) e (df : {O_F e}) : bigO_def F (- (df : _ -> _)) e.
proof: Proof. have := bigOP [bigO of df]; apply: filter_app; near=> k. by apply: filter_app; near=> x; rewrite normrN. 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