proposition: Theorem Rnd_N_pt_DN_or_UP_eq : forall F : R -> Prop, forall x fd fu f : R, Rnd_DN_pt F x fd -> Rnd_UP_pt F x fu -> Rnd_N_pt F x f -> f = fd \/ f = fu.
proof: Proof. intros F x fd fu f Hd Hu Hf. destruct (Rnd_N_pt_DN_or_UP F x f Hf) as [H|H]. left. apply Rnd_DN_pt_unique with (1 := H) (2 := Hd). right. apply Rnd_UP_pt_unique with (1 := H) (2 := Hu). Qed.
imports: Coq(Reals) Raux Defs