proposition: Theorem round_UP_DN_ulp : forall x, ~ F x -> round beta fexp Zceil x = (round beta fexp Zfloor x + ulp x)%R.
proof: Proof. intros x Fx. rewrite ulp_neq_0. unfold round. simpl. unfold F2R. simpl. rewrite Zceil_floor_neq. rewrite plus_IZR. simpl. ring. intros H. apply Fx. unfold generic_format, F2R. simpl. rewrite <- H. rewrite Ztrunc_IZR. rewrite H. now rewrite scaled_mantissa_mult_bpow. intros V; apply Fx. rewrite V. apply generic_format_0. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop