proposition: Lemma deriv_1_deriv : Feq I (PartInt (ProjT1 diffF)) (PartInt (ProjT1 (Diffble_I_n_imp_deriv_n _ _ diffFn))).
proof: Proof. intros. simpl in |- *. unfold I, Hab in |- *; apply Derivative_I_unique with F. apply projT2. cut (Derivative_I_n Hab' 1 F (PartInt (ProjT1 (Diffble_I_n_imp_deriv_n 1 F diffFn)))). 2: apply projT2. intro H. elim H; intros f' H0 H1. apply Derivative_I_wdr with (PartInt f'); assumption. Qed.
imports: CoRN.ftc.Differentiability