proposition: Lemma Diffble_I_n_wd : forall n F G, Feq I F G -> Diffble_I_n Hab' n F -> Diffble_I_n Hab' n G.
proof: Proof. intro. induction n as [| n Hrecn]. simpl in |- *; unfold Feq in |- *; tauto. intros F G H H0. elim H0; intros H1 H2; clear H0. cut (Diffble_I Hab' G). 2: apply Diffble_I_wd with F; assumption. intro H0. exists H0. eapply Hrecn. 2: apply H2. 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