proposition: Lemma deriv_restr : forall Hab' (f : deriv_function), Derivative_I (a:=a) (b:=b) Hab' (deriv_to_pfunct f) (deriv_deriv 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 |- *. assumption. apply projT2. exact (Derivative_I_const _ _ Hab' c). exact (Derivative_I_id _ _ Hab'). exact (Derivative_I_plus _ _ _ _ _ _ _ Hrecf1 Hrecf0). exact (Derivative_I_inv _ _ _ _ _ Hrecf). exact (Derivative_I_minus _ _ _ _ _ _ _ Hrecf1 Hrecf0). exact (Derivative_I_mult _ _ _ _ _ _ _ Hrecf1 Hrecf0). exact (Derivative_I_scal _ _ _ _ _ Hrecf _). case n. apply Derivative_I_wdl with (Fconst (S:=IR) [1]). apply FNth_zero'. exact (derivative_imp_inc _ _ _ _ _ Hrecf). exact (Derivative_I_const _ _ Hab' _). clear n; intro. exact (Derivative_I_nth _ _ _ _ _ Hrecf n). Qed.
imports: CoRN.ftc.Differentiability