proposition: Lemma equiv_ext_loc {F : (T -> Prop) -> Prop} {FF : Filter F} (f g : T -> V) : F (fun x => f x = g x) -> is_equiv F f g.
proof: Proof. move => H eps. move: H ; apply filter_imp. move => 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