proposition: Lemma opp_littleo_subproof (F : filter_on T) e (df : {o_F e}) : littleo_def F (- (df : _ -> _)) e.
proof: Proof. by move=> _/posnumP[eps]; near do rewrite normrN; 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