proposition: Lemma Derivative_n_plus : forall J pJ n m k F G H, Derivative_n m J pJ F G -> Derivative_n n J pJ G H -> k = m + n -> Derivative_n k J pJ F H.
proof: Proof. intros J pJ n m k F G H H0 H1 H2. elim H0; intros incF Hf. elim Hf; intros incG derFG. elim H1; intros incG' Hg. elim Hg; intros incH derGH. clear Hf Hg. split; auto. split; auto. intros; apply Derivative_I_n_plus with n m G; auto. Qed.
imports: CoRN.ftc.MoreIntervals