proposition: Lemma filterdiff_comp' f g x (lf : U -> V) (lg : V -> W) : filterdiff f (locally x) lf -> filterdiff g (locally (f x)) lg -> filterdiff (fun y => g (f y)) (locally x) (fun y => lg (lf y)).
proof: Proof. intros. apply filterdiff_comp. by []. apply filterdiff_locally with (f x). apply is_filter_lim_filtermap => //. apply filterdiff_continuous => //. eexists ; by apply H. by []. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv