proposition: Lemma n_deriv_plus : forall m n F H H', Derivative_I_n Hab' m (n_deriv_I n F H) (n_deriv_I (m + n) F H').
proof: Proof. intro; induction m as [| m Hrecm]. simpl in |- *. intros. apply n_deriv_I_wd. unfold I in |- *; apply Feq_reflexive. exact (Diffble_I_n_imp_inc _ _ _ _ _ H). intros. simpl in |- *. cut (Diffble_I_n Hab' (S n) F). intro H0. exists (IntPartIR (n_deriv_inc _ _ H0)). eapply Derivative_I_wdr. 2: apply n_Sn_deriv with (HS := H0). FEQ. apply n_deriv_inc. cut (Diffble_I_n Hab' (m + n) (PartInt (ProjT1 (Diffble_I_n_imp_diffble _ _ _ (S n) (Nat.lt_0_succ n) F H0)))). intro H1. eapply Derivative_I_n_wdr. 2: eapply Derivative_I_n_wdl. 3: apply Hrecm with (H' := H1). apply n_deriv_I_wd. unfold I, Hab in |- *; apply Derivative_I_unique with F. apply projT2. apply projT2. FEQ. apply n_deriv_inc. simpl in |- *; algebra. elim H'; intros. eapply Diffble_I_n_wd. 2: apply p. apply Derivative_I_unique with F. apply projT2. apply projT2. apply le_imp_Diffble_I with (S m + n). simpl in |- *; rewrite Nat.add_comm; auto with arith. assumption. Qed.
imports: CoRN.ftc.Differentiability