proposition: Lemma FRestr_bnd : forall (HP : pred_wd _ P) (H : included P (Dom F)), included Q P -> bnd_away_zero Q F -> bnd_away_zero Q (Frestr HP H).
proof: Proof. intros HP H H0 H1. elim H1; clear H1; intros H2 H3; split. auto. elim H3; intro c; intros. exists c; simpl in |- *; auto. Qed.
imports: CoRN.reals.Intervals CoRN.tactics.DiffTactics1