proposition: Lemma continuity_pt_comp : forall f1 f2 z, continuity_pt f1 z -> continuity_pt f2 (f1 z) -> continuity_pt (comp f2 f1) z.
proof: Proof. intros f1 f2 z Hf1 Hf2 eps eps_pos ; unfold comp. cut (limit1_in (fun z => f2 (f1 z)) (Dgf (D_x no_cond z) (D_x no_cond (f1 z)) f1) (f2 (f1 z)) z -> limit1_in (fun z => f2 (f1 z)) (D_x no_cond z) (f2 (f1 z)) z). intro H ; apply H. eapply limit_comp ; [apply Hf1 | apply Hf2]. assumption. intros H eps' eps'_pos ; destruct (H eps' eps'_pos) as (delta,[delta_pos Hdelta]) ; clear H ; exists delta ; split ; [assumption |]. intros z' [H Hz']. case (Ceq_dec (f1 z) (f1 z')) ; intro Heq. simpl ; unfold C_dist ; rewrite Heq. unfold Cminus ; rewrite Cadd_opp_r ; rewrite Cnorm_C0 ; assumption. apply Hdelta ; split. unfold Dgf ; unfold D_x ; repeat split. intro Hf ; apply Heq ; subst ; reflexivity. assumption. assumption. Qed.
imports: Cfunctions Cprop_base Cbase Canalysis_def