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