proposition: Lemma continuous_cont : forall Hab (f : cont_function), Continuous_I (a:=a) (b:=b) Hab (cont_to_pfunct f).
proof: Proof. intros. induction f as [Hab0 F c| Hab' F F' d| Hab' F F' d| Hab' F d| c| | f1 Hrecf1 f0 Hrecf0| f Hrecf| f1 Hrecf1 f0 Hrecf0| f1 Hrecf1 f0 Hrecf0| c f Hrecf| f Hrecf n| f Hrecf]; simpl in |- *; intros. assumption. exact (deriv_imp_contin_I _ _ _ _ _ _ d). exact (deriv_imp_contin'_I _ _ _ _ _ _ d). exact (diffble_imp_contin_I _ _ _ _ _ d). exact (Continuous_I_const _ _ _ c). exact (Continuous_I_id _ _ _). exact (Continuous_I_plus _ _ _ _ _ Hrecf1 Hrecf0). exact (Continuous_I_inv _ _ _ _ Hrecf). exact (Continuous_I_minus _ _ _ _ _ Hrecf1 Hrecf0). exact (Continuous_I_mult _ _ _ _ _ Hrecf1 Hrecf0). exact (Continuous_I_scal _ _ _ _ Hrecf _). exact (Continuous_I_nth _ _ _ _ Hrecf _). exact (Continuous_I_abs _ _ _ _ Hrecf). Qed.
imports: CoRN.ftc.Differentiability