proposition: Lemma littleoE (tag : unit) (F : filter_on T) (phF : phantom (set_system T) F) f h : littleo_def F f h -> the_littleo tag F phF f h = f.
proof: Proof. by move=> /asboolP?; rewrite /the_littleo /insubd insubT. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule