proposition: Fact ex12 : forall x f, Rnd_N_pt F x f -> Rnd_DN_pt F x f \/ Rnd_UP_pt F x f.
proof: Proof. intros x f [Ff Pf]. destruct (Rle_dec x f) as [xLf|xGf]. - right; repeat split; auto. intros g Fg xLg. assert (Hg := Pf g Fg). rewrite !Rabs_right in Hg; lra. - left; repeat split; try lra; auto. intros g Fg gLx. assert (Hg := Pf g Fg). rewrite !Rabs_left1 in Hg; lra. Qed.
imports: Psatz Reals Flocq(Core)