proposition: Lemma N_Deriv_plus : forall m n F H H', Derivative_n m I pI (N_Deriv n F H) (N_Deriv (m + n) F H').
proof: Proof. intros. split; Included. split; Included. intros a b Hab H0. cut (Diffble_I_n Hab n F). intro H1. cut (Diffble_I_n Hab (m + n) F). intro H2. eapply Derivative_I_n_wdl. apply Feq_symmetric; apply (N_Deriv_Feq n F H _ _ Hab H1 H0). eapply Derivative_I_n_wdr. apply Feq_symmetric; apply (N_Deriv_Feq _ _ H' _ _ Hab H2 H0). apply n_deriv_plus. elim H'; auto. elim H; auto. Qed.
imports: CoRN.ftc.MoreIntervals