proposition: Lemma Diffble_imp_Diffble_n : Diffble_n 1 I pI F.
proof: Proof. elim diffF; intros incF diffbleF. split; auto. intros a b Hab H; exists (diffbleF a b Hab H). simpl in |- *; Included. Qed.
imports: CoRN.ftc.MoreIntervals