proposition: Lemma ex_filterdiff_comp'_2 : forall (f : T -> U) (g : T -> V) (h : U -> V -> W) x, ex_filterdiff f (locally x) -> ex_filterdiff g (locally x) -> ex_filterdiff (fun t => h (fst t) (snd t)) (locally (f x,g x)) -> ex_filterdiff (fun y : T => h (f y) (g y)) (locally x).
proof: Proof. intros f g h x [lf Df] [lg Dg] [lh Dh]. exists (fun x => lh (lf x,lg x)). apply (filterdiff_comp'_2 f g h x lf lg (fun x y => lh (x,y))) ; try eassumption. eapply filterdiff_ext_lin ; try eassumption. by case. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv