proposition: Lemma Diffble_n_imp_le : forall n, 0 < n -> forall F F', Diffble_n n I pI F -> Derivative I pI F F' -> Diffble_n (pred n) I pI F'.
proof: Proof. intros n H F F' H0 H1. elim H0; intros incF diffF. elim H1; intros incFa H2. elim H2; intros incF' derivF. split; auto. intros; apply Diffble_I_imp_le with F; auto. Qed.
imports: CoRN.ftc.MoreIntervals