proposition: Lemma diffble_restr : forall Hab' (f : deriv_function), Diffble_I (a:=a) (b:=b) Hab' (deriv_to_pfunct f).
proof: Proof. intros. induction f as [Hab'0 f f' d| Hab'0 f d| c| | f1 Hrecf1 f0 Hrecf0| f Hrecf| f1 Hrecf1 f0 Hrecf0| f1 Hrecf1 f0 Hrecf0| c f Hrecf| f Hrecf n]; simpl in |- *. apply deriv_imp_Diffble_I with f'; assumption. assumption. exact (Diffble_I_const _ _ Hab' c). exact (Diffble_I_id _ _ Hab'). exact (Diffble_I_plus _ _ _ _ _ Hrecf1 Hrecf0). exact (Diffble_I_inv _ _ _ _ Hrecf). exact (Diffble_I_minus _ _ _ _ _ Hrecf1 Hrecf0). exact (Diffble_I_mult _ _ _ _ _ Hrecf1 Hrecf0). exact (Diffble_I_scal _ _ _ _ Hrecf _). exact (Diffble_I_nth _ _ _ _ Hrecf n). Qed.
imports: CoRN.ftc.Differentiability