proposition: Lemma n_Sn_deriv : forall n F H HS, Derivative_I Hab' (n_deriv_I n F H) (n_deriv_I (S n) F HS).
proof: Proof. intro; induction n as [| n Hrecn]. intros. apply Derivative_I_wdl with F. FEQ. apply Derivative_I_wdr with (PartInt (ProjT1 (Diffble_I_n_imp_diffble _ _ _ _ (Nat.lt_0_succ 0) _ HS))). apply eq_imp_Feq. Included. Included. intros; simpl in |- *; apply csf_wd_unfolded; simpl in |- *; algebra. apply projT2. intro. cut {p : nat | p = S n}. intro H; elim H; intros p H0. pattern (S n) at 2 4 in |- *; rewrite <- H0. intros. elim H1; intros H0' H0''; clear H1. elim HS; intros H1' H1''; clear HS. cut (Diffble_I_n Hab' n (PartInt (ProjT1 H1'))). intro H1'''. apply Derivative_I_wdl with (n_deriv_I _ _ H1'''). 2: apply Derivative_I_wdr with (n_deriv_I _ _ H1''). simpl in |- *; apply n_deriv_I_wd. unfold I, Hab in |- *; apply Derivative_I_unique with F. apply projT2. apply projT2. simpl in |- *; apply n_deriv_I_wd. unfold I, Hab in |- *; apply Derivative_I_unique with F. apply projT2. apply projT2. generalize H1''. rewrite H0. intro. apply Hrecn. generalize H1''; clear H1''. rewrite H0; intro. apply le_imp_Diffble_I with (S n); [ auto with arith | assumption ]. exists (S n); auto. Qed.
imports: CoRN.ftc.Differentiability