proposition: Theorem Rnd_N_pt_UP : forall F : R -> Prop, forall x d u : R, Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> (u - x <= x - d)%R -> Rnd_N_pt F x u.
proof: Proof. intros F x d u Hd Hu Hx. assert (Hux: (Rabs (u - x) = u - x)%R). apply Rabs_pos_eq. apply Rle_0_minus. apply Hu. apply Rnd_N_pt_DN_UP with (2 := Hd) (3 := Hu). apply Hu. now rewrite Hux. rewrite Hux. apply Rle_refl. Qed.
imports: Coq(Reals) Raux Defs