proposition: Lemma equiv_plus : forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f o : T -> V), is_domin F f o -> is_equiv F (fun x => plus (f x) (o x)) f.
proof: Proof. intros F FF f o H eps. move: (H eps) => {H}. apply filter_imp => x Hx. simpl. now rewrite /minus opp_plus plus_assoc plus_opp_r plus_zero_l norm_opp. Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy