proposition: Lemma ex_filterdiff_comp {F} {FF : Filter F} (f : U -> V) (g : V -> W) : ex_filterdiff f F -> ex_filterdiff g (filtermap f F) -> ex_filterdiff (fun y => g (f y)) F.
proof: Proof. intros [lf Df] [lg Dg]. eexists ; eapply filterdiff_comp ; eassumption. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv