proposition: Lemma add_bigO_subproof (F : filter_on T) e (df dg : {O_F e}) : bigO_def F (df \+ dg) e.
proof: Proof. near=> k; near=> x; apply: le_trans (ler_normD _ _) _. by rewrite (splitr k) mulrDl lerD //; near: x; near: k; [apply: near_pinfty_div2 (bigOP df)|apply: near_pinfty_div2 (bigOP dg)]. 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