proposition: Theorem round_N_middle : forall x, (x - round Zfloor x = round Zceil x - x)%R -> round Znearest x = if choice (Zfloor (scaled_mantissa x)) then round Zceil x else round Zfloor x.
proof: Proof. intros x. pattern x at 1 4 ; rewrite <- scaled_mantissa_mult_bpow. unfold round, Znearest, F2R. simpl. destruct (Req_dec (IZR (Zfloor (scaled_mantissa x))) (scaled_mantissa x)) as [Fx|Fx]. intros _. rewrite <- Fx. rewrite Zceil_IZR, Zfloor_IZR. set (m := Zfloor (scaled_mantissa x)). now case (Rcompare (IZR m - IZR m) (/ 2)) ; case (choice m). intros H. rewrite Rcompare_floor_ceil_middle with (1 := Fx). rewrite Rcompare_Eq. now case choice. apply Rmult_eq_reg_r with (bpow (cexp x)). now rewrite 2!Rmult_minus_distr_r. apply Rgt_not_eq. apply bpow_gt_0. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop