proposition: Lemma Derivative_I_n_plus : forall n m k F G H, Derivative_I_n Hab' m F G -> Derivative_I_n Hab' n G H -> k = m + n -> Derivative_I_n Hab' k F H.
proof: Proof. do 2 intro. induction m as [| m Hrecm]; intros k F G H H0 H1 H2; rewrite H2. simpl in |- *. apply Derivative_I_n_wdl with G. elim H0; clear H0; intros H3 H4. elim H4; clear H4; intros H0 H5. apply Derivative_I_n_unique with 0 G. simpl in |- *; apply Feq_reflexive; auto. simpl in |- *; FEQ; algebra. auto. elim H0; intros F' H3 H4. exists F'; auto. apply Hrecm with G; auto. Qed.
imports: CoRN.ftc.Differentiability