proposition: Fact ex10 : round_pred (Rnd_ZR_pt F).
proof: Proof. split. - intros x. destruct (Req_dec x 0) as [xE0 | xD0]. exists 0; rewrite xE0. apply ex5; destruct SAF; auto. destruct ex8 as [DP _]. destruct (DP x) as [f1 Hf1]. destruct ex9 as [UP _]. destruct (UP x) as [f2 Hf2]. destruct (Rle_dec 0 x) as [xPos | xNPos]. exists f1; split; try lra; auto. exists f2; split; try lra; auto. - apply ex6; destruct SAF; auto. Qed.
imports: Psatz Reals Flocq(Core)