proposition: Lemma filterdiff_ext_loc {F} {FF : Filter F} (f g : U -> V) (l : U -> V) : F (fun y => f y = g y) -> (forall x, is_filter_lim F x -> f x = g x) -> filterdiff f F l -> filterdiff g F l.
proof: Proof. move => H H0 [Hl Df]. split => //. move => x Hx eps. specialize (H0 x Hx). specialize (Df x Hx eps). apply filter_and with (1 := H) in Df. move: Df ; apply filter_imp => y [Hy]. apply Rle_trans. by apply Req_le ; rewrite Hy H0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv