proposition: Lemma filterdiff_ext {F} {FF : Filter F} (f g : U -> V) (l : U -> V) : (forall y , f y = g y) -> filterdiff f F l -> filterdiff g F l.
proof: Proof. move => H. apply filterdiff_ext_loc => //. now apply filter_forall. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv