proposition: Lemma equiv_carac_1 : forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f g o : T -> V), (forall x, f x = plus (g x) (o x)) -> is_domin F g o -> is_equiv F f g.
proof: Proof. intros F FF f g o Ho Hgo. intro eps ; move: (Hgo eps). apply filter_imp => x. replace (o x) with (minus (f x) (g x)). congr (_ <= _). by rewrite -norm_opp /minus opp_plus opp_opp plus_comm. rewrite Ho. rewrite /minus plus_comm plus_assoc plus_opp_l. apply plus_zero_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy