proposition: Lemma equiv_refl : forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f : T -> V), is_equiv F f f.
proof: Proof. intros F FF f eps. apply: filter_forall => x. rewrite /minus plus_opp_r norm_zero. apply Rmult_le_pos. by apply Rlt_le, eps. by apply norm_ge_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy