proposition: Lemma equiv_trans : forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f g h : T -> V), is_equiv F f g -> is_equiv F g h -> is_equiv F f h.
proof: Proof. intros F FF f g h Hfg Hgh. apply (fun c => domin_rw_l _ _ c Hgh). intros eps. apply equiv_sym in Hgh. generalize (filter_and _ _ (Hfg (pos_div_2 eps)) (Hgh (pos_div_2 eps))) => {Hfg Hgh}. apply filter_imp => x /= [Hfg Hgh]. replace (minus (h x) (f x)) with (plus (minus (g x) (f x)) (opp (minus (g x) (h x)))). eapply Rle_trans. 1 : by apply @norm_triangle. rewrite norm_opp (double_var eps) Rmult_plus_distr_r. by apply Rplus_le_compat. rewrite /minus opp_plus opp_opp plus_comm plus_assoc. congr (plus _ (opp (f x))). rewrite plus_comm plus_assoc plus_opp_r. apply plus_zero_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy