proposition: Lemma Included_imp_Diffble_n : forall n (J : interval) pJ F, included J I -> Diffble_n n I pI F -> Diffble_n n J pJ F.
proof: Proof. intros n J pJ F H H0. elim H0; clear H0; intros H1 H2. split. Included. intros; apply H2. Included. Qed.
imports: CoRN.ftc.MoreIntervals