proposition: Lemma n_deriv_I_wd : forall n F G Hf Hg, Feq I F G -> Feq I (n_deriv_I n F Hf) (n_deriv_I n G Hg).
proof: Proof. intro; induction n as [| n Hrecn]; intros F G Hf Hg H. elim H; clear H; intros H H0. elim H0; clear H0; intros H2 H1. unfold I in |- *; simpl in |- *; FEQ. simpl in |- *; apply H1; auto. simpl in |- *. apply Hrecn. unfold I, Hab in |- *; apply Derivative_I_unique with F. apply projT2. apply Derivative_I_wdl with G. apply Feq_symmetric; assumption. apply projT2. Qed.
imports: CoRN.ftc.Differentiability