proposition: Lemma domin_plus : forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f : T -> U) (g1 g2 : T -> V), is_domin F f g1 -> is_domin F f g2 -> is_domin F f (fun x => plus (g1 x) (g2 x)).
proof: Proof. intros F FF f g1 g2 Hg1 Hg2 eps. generalize (filter_and _ _ (Hg1 (pos_div_2 eps)) (Hg2 (pos_div_2 eps))) => /= {Hg1 Hg2}. apply filter_imp => x [Hg1 Hg2]. eapply Rle_trans. apply @norm_triangle. eapply Rle_trans. apply Rplus_le_compat. by apply Hg1. by apply Hg2. apply Req_le ; field. Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy