proposition: Lemma Diffble_I_n_imp_deriv_n : forall n F, Diffble_I_n Hab' n F -> {f' : CSetoid_fun (subset (Compact Hab)) IR | Derivative_I_n Hab' n F (PartInt f')}.
proof: Proof. intro; induction n as [| n Hrecn]. intros F H. exists (IntPartIR (Diffble_I_n_imp_inc _ _ H)). simpl in |- *; simpl in H. FEQ. intros F H. elim H; intros H1 H2. elim (Hrecn _ H2); intros f' Hf'. exists f'. simpl in |- *. exists (ProjT1 H1). apply projT2. assumption. Qed.
imports: CoRN.ftc.Differentiability