proposition: Lemma Diffble_n_wd : forall n F G, Feq I F G -> Diffble_n n I pI F -> Diffble_n n I pI G.
proof: Proof. intros n F G H H0. elim H; intros incF H1. elim H1; intro incG. split. auto. intros; apply Diffble_I_n_wd with F. apply included_Feq with I; auto. elim H0; auto. Qed.
imports: CoRN.ftc.MoreIntervals