proposition: Lemma equiv_carac_0 : forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f g : T -> V), is_equiv F f g -> {o : T -> V | (forall x : T, f x = plus (g x) (o x)) /\ is_domin F g o }.
proof: Proof. intros F FF f g H. exists (fun x => minus (f x) (g x)). split. intro x. by rewrite /minus plus_comm -plus_assoc plus_opp_l plus_zero_r. apply (domin_rw_l _ _ _ H). by apply equiv_sym. Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy