proposition: Theorem Rnd_N_pt_DN_UP : forall F : R -> Prop, forall x d u f : R, F f -> Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> (Rabs (f - x) <= x - d)%R -> (Rabs (f - x) <= u - x)%R -> Rnd_N_pt F x f.
proof: Proof. intros F x d u f Hf Hxd Hxu Hd Hu. split. exact Hf. intros g Hg. destruct (Rnd_DN_UP_pt_split F x d u Hxd Hxu g Hg) as [Hgd|Hgu]. apply Rle_trans with (1 := Hd). rewrite Rabs_left1. rewrite Ropp_minus_distr. apply Rplus_le_compat_l. now apply Ropp_le_contravar. apply Rle_minus. apply Rle_trans with (1 := Hgd). apply Hxd. apply Rle_trans with (1 := Hu). rewrite Rabs_pos_eq. now apply Rplus_le_compat_r. apply Rle_0_minus. apply Rle_trans with (2 := Hgu). apply Hxu. Qed.
imports: Coq(Reals) Raux Defs