proposition: Fact ex9 : round_pred (Rnd_UP_pt F).
proof: Proof. destruct SAF as [F0 Fsym DNtotal]. split. - intros x. destruct (DNtotal (-x)) as [f [Ff [fLNx Pf]]]. exists (- f); repeat split; try lra. apply Fsym; auto. intros g Fx xLg. assert (-g <= f). apply Pf; try lra. apply Fsym; auto. lra. - apply ex4. Qed.
imports: Psatz Reals Flocq(Core)