proposition: Lemma le_imp_Diffble_n : forall m n, m <= n -> forall F, Diffble_n n I pI F -> Diffble_n m I pI F.
proof: Proof. intros m n H F H0. elim H0; intros incF diffF. split; auto. intros; apply le_imp_Diffble_I with n; auto. Qed.
imports: CoRN.ftc.MoreIntervals