proposition: Lemma Diffble_n_imp_Diffble : forall n : nat, 0 < n -> forall F, Diffble_n n I pI F -> Diffble I pI F.
proof: Proof. intros n H F H0. elim H0; intros incF diffF. split; auto. intros; apply Diffble_I_n_imp_diffble with n; auto. Qed.
imports: CoRN.ftc.MoreIntervals