proposition: Lemma Derivative_comp : Derivative I pI F F' -> Derivative J pJ G G' -> Derivative I pI (G[o]F) ((G'[o]F) {*}F').
proof: Proof. clear Hmap. assert (Hmap := maps_compacts_into_strict_imp_weak F Hmap'). intros H H0. elim H; clear H; intros incF H'. elim H'; clear H'; intros incF' derF. elim H0; clear H0; intros incG H'. elim H'; clear H'; intros incG' derG. split. simpl in |- *; red in |- *; intros x H; exists (incF _ H). apply incG; apply comp_inc_lemma; auto. split. apply included_FMult. simpl in |- *; red in |- *; intros x H; exists (incF _ H). apply incG'; apply comp_inc_lemma; auto. Included. intros a b Hab H. elim (Hmap' _ _ (less_leEq _ _ _ Hab) H); clear Hmap'; intros c Hc. elim Hc; clear Hc; intros d Hd. elim Hd; clear Hd; intros Hcd Hmap2. inversion_clear Hmap2. apply Derivative_I_comp with c d Hcd; auto. red in |- *; intros. split; auto. Included. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries