proposition: Lemma Continuous_comp : Continuous I F -> Continuous J G -> Continuous I (G[o]F).
proof: Proof. intros H H0. elim H; clear H; intros incF contF. elim H0; clear H0; intros incG contG. split. intros x H. exists (incF _ H). apply incG. apply comp_inc_lemma; auto. intros a b Hab H. elim (Hmap _ _ Hab H); clear Hmap; intros c Hc. elim Hc; clear Hc; intros d Hd. elim Hd; clear Hd; intros Hcd Hmap'. inversion_clear Hmap'. apply Continuous_I_comp with c d Hcd; auto. red in |- *; intros. split; auto. Included. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries