proposition: Lemma equiv_sym : forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f g : T -> V), is_equiv F f g -> is_equiv F g f.
proof: Proof. intros F FF f g H eps. assert (H0 := equiv_le_2 _ _ _ H). specialize (H (pos_div_2 eps)). generalize (filter_and _ _ H H0) ; apply filter_imp ; clear => x [H [H0 H1]]. rewrite -norm_opp /minus opp_plus opp_opp plus_comm. apply Rle_trans with (1 := H) ; simpl. eapply Rle_trans. apply Rmult_le_compat_l. by apply Rlt_le, is_pos_div_2. by apply H0. apply Req_le ; field. Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy