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