proposition: Lemma FRestr_bnd' : forall (HP : pred_wd _ P) (H : included P (Dom F)), bnd_away_zero_everywhere F -> bnd_away_zero_everywhere (Frestr HP H).
proof: Proof. intros HP H H0 a b Hab H1. elim (H0 a b Hab); intros. split. auto. elim b0; intro c; intros. exists c; simpl in |- *; auto. apply included_trans with P; simpl in H1; auto. Qed.
imports: CoRN.reals.Intervals CoRN.tactics.DiffTactics1