proposition: Theorem Rnd_NE_pt_total : round_pred_total Rnd_NE_pt.
proof: Proof. apply satisfies_any_imp_NG. now apply generic_format_satisfies_any. intros x d u Hf Hd Hu. generalize (proj1 Hd). unfold generic_format. set (ed := cexp beta fexp d). set (md := Ztrunc (scaled_mantissa beta fexp d)). intros Hd1. case_eq (Z.even md) ; [ intros He | intros Ho ]. right. exists (Float beta md ed). unfold Generic_fmt.canonical. rewrite <- Hd1. now repeat split. left. generalize (proj1 Hu). unfold generic_format. set (eu := cexp beta fexp u). set (mu := Ztrunc (scaled_mantissa beta fexp u)). intros Hu1. rewrite Hu1. eexists ; repeat split. unfold Generic_fmt.canonical. now rewrite <- Hu1. rewrite (DN_UP_parity_generic x (Float beta md ed) (Float beta mu eu)). simpl. now rewrite Ho. exact Hf. unfold Generic_fmt.canonical. now rewrite <- Hd1. unfold Generic_fmt.canonical. now rewrite <- Hu1. rewrite <- Hd1. apply Rnd_DN_pt_unique with (1 := Hd). now apply round_DN_pt. rewrite <- Hu1. apply Rnd_UP_pt_unique with (1 := Hu). now apply round_UP_pt. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp