proposition: Lemma bnd_imp_inc_div : forall G, included I (Dom G) -> included I (Dom (G{/}F)).
proof: Proof. intros G HG x Hx. split; auto. elim Hf; intros H0 H1. split. apply (H0 x Hx). intro. apply bnd_imp_ap_zero; auto. Qed.
imports: CoRN.reals.Intervals CoRN.tactics.DiffTactics1