proposition: Theorem round_NA_pt : forall x, Rnd_NA_pt generic_format x (round (Znearest (Zle_bool 0)) x).
proof: Proof. intros x. generalize (round_N_pt (Zle_bool 0) x). set (f := round (Znearest (Zle_bool 0)) x). intros Rxf. destruct (Req_dec (x - round Zfloor x) (round Zceil x - x)) as [Hm|Hm]. apply Rnd_NA_pt_N. exact generic_format_0. exact Rxf. destruct (Rle_or_lt 0 x) as [Hx|Hx]. rewrite Rabs_pos_eq with (1 := Hx). rewrite Rabs_pos_eq. unfold f. rewrite round_N_middle with (1 := Hm). rewrite Zle_bool_true. apply (round_UP_pt x). apply Zfloor_lub. apply Rmult_le_pos with (1 := Hx). apply bpow_ge_0. apply Rnd_N_pt_ge_0 with (2 := Hx) (3 := Rxf). exact generic_format_0. rewrite Rabs_left with (1 := Hx). rewrite Rabs_left1. apply Ropp_le_contravar. unfold f. rewrite round_N_middle with (1 := Hm). rewrite Zle_bool_false. apply (round_DN_pt x). apply lt_IZR. apply Rle_lt_trans with (scaled_mantissa x). apply Zfloor_lb. simpl. rewrite <- (Rmult_0_l (bpow (- cexp x))). apply Rmult_lt_compat_r with (2 := Hx). apply bpow_gt_0. apply Rnd_N_pt_le_0 with (3 := Rxf). exact generic_format_0. now apply Rlt_le. split. apply Rxf. intros g Rxg. rewrite Rnd_N_pt_unique with (3 := Hm) (4 := Rxf) (5 := Rxg). apply Rle_refl. apply round_DN_pt. apply round_UP_pt. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop