proposition: Lemma Derivative_I_n_imp_inc' : forall n F F', Derivative_I_n Hab' n F F' -> included I (Dom F').
proof: Proof. intro; induction n as [| n Hrecn]; intros F F' H. simpl in |- *; simpl in H. elim H; intros H0 H1; elim H1; auto. elim H; intros f' H0 H1. apply Hrecn with (PartInt f'). assumption. Qed.
imports: CoRN.ftc.Differentiability