proposition: Lemma bnd_imp_inc_recip : included I (Dom {1/}F).
proof: Proof. intros x Hx. elim Hf; intros H H0. split. apply (H x Hx). intro. apply bnd_imp_ap_zero; auto. Qed.
imports: CoRN.reals.Intervals CoRN.tactics.DiffTactics1