proposition: Lemma Diffble_comp : forall I J pI pJ F G, maps_compacts_into I J F -> Diffble I pI F -> Diffble J pJ G -> Diffble I pI (G[o]F).
proof: Proof. intros I J pI pJ F G H H0 H1. apply Derivative_imp_Diffble with ((Deriv _ _ _ H1[o]F) {*}Deriv _ _ _ H0). apply Derivative_comp with J pJ; auto; apply Deriv_lemma. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries