proposition: Lemma included_imp_bnd : included Q P -> bnd_away_zero P F -> bnd_away_zero Q F.
proof: Proof. intros H H0. elim H0; clear H0; intros H1 H2; split. apply included_trans with P; auto. elim H2; intros c Hc Hc'. exists c; auto. Qed.
imports: CoRN.reals.Intervals CoRN.tactics.DiffTactics1