proposition: Theorem Rnd_N_pt_DN_or_UP : forall F : R -> Prop, forall x f : R, Rnd_N_pt F x f -> Rnd_DN_pt F x f \/ Rnd_UP_pt F x f.
proof: Proof. intros F x f (Hf1,Hf2). destruct (Rle_or_lt x f) as [Hxf|Hxf]. right. repeat split ; try assumption. intros g Hg Hxg. specialize (Hf2 g Hg). rewrite 2!Rabs_pos_eq in Hf2. now apply Rplus_le_reg_r with (-x)%R. now apply Rle_0_minus. now apply Rle_0_minus. left. repeat split ; try assumption. now apply Rlt_le. intros g Hg Hxg. specialize (Hf2 g Hg). rewrite 2!Rabs_left1 in Hf2. generalize (Ropp_le_cancel _ _ Hf2). intros H. now apply Rplus_le_reg_r with (-x)%R. now apply Rle_minus. apply Rlt_le. now apply Rlt_minus. Qed.
imports: Coq(Reals) Raux Defs