proposition: Lemma filterdiff_locally {F} {FF : ProperFilter F} (f : U -> V) x l : is_filter_lim F x -> filterdiff f (locally x) l -> filterdiff f F l.
proof: Proof. intros Fx [Hl Df]. split. exact Hl. intros z Fz. specialize (Df _ (fun P H => H)). generalize (is_filter_lim_unique _ _ Fx Fz). intros ->. now apply is_domin_le with (2 := Fz). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv