proposition: Lemma eqadd_some_oP (F : filter_on T) (f g : T -> V) (e : T -> W) h : f = g + [o_F e of h] -> littleo_def F (f - g) e.
proof: Proof. rewrite /the_littleo /insubd=> ->. case: insubP => /= [u /asboolP fg_o_e ->|_] eps /=. by rewrite addrAC subrr add0r; apply: fg_o_e. by rewrite addrC addKr; apply: littleoP. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule