proposition: Lemma add_littleo_subproof (F : filter_on T) e (df dg : {o_F e}) : littleo_def F (df \+ dg) e.
proof: Proof. by move=> _/posnumP[eps]; near do [ rewrite [eps%:num]splitr mulrDl (le_trans (ler_normD _ _)) // lerD //]; 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