proposition: Lemma addOmega (R : realFieldType) (F : filter_on pT) (f g h : _ -> R^o) (f_nonneg : forall x, 0 <= f x) (g_nonneg : forall x, 0 <= g x) : f =Omega_F h -> f + g =Omega_F h.
proof: Proof. rewrite 2!eqOmegaE !eqOmegaO => /eqOP hOf; apply/eqOP. apply: filter_app hOf; near=> k; apply: filter_app; near=> x => /le_trans. by apply; rewrite ler_pM2l // !ger0_norm // ?addr_ge0 // lerDl. 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