proposition: Theorem round_bounded_large_pos : forall x ex, (fexp ex < ex)%Z -> (bpow (ex - 1) <= x < bpow ex)%R -> (bpow (ex - 1) <= round x <= bpow ex)%R.
proof: Proof. intros x ex He Hx. unfold round, scaled_mantissa. rewrite (cexp_fexp_pos _ _ Hx). unfold F2R. simpl. destruct (Zrnd_DN_or_UP (x * bpow (- fexp ex))) as [Hr|Hr] ; rewrite Hr. split. replace (ex - 1)%Z with (ex - 1 + - fexp ex + fexp ex)%Z by ring. rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. assert (Hf: IZR (Zpower beta (ex - 1 - fexp ex)) = bpow (ex - 1 + - fexp ex)). apply IZR_Zpower. lia. rewrite <- Hf. apply IZR_le. apply Zfloor_lub. rewrite Hf. rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. apply Hx. apply Rle_trans with (2 := Rlt_le _ _ (proj2 Hx)). apply Rmult_le_reg_r with (bpow (- fexp ex)). apply bpow_gt_0. rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r. apply Zfloor_lb. split. apply Rle_trans with (1 := proj1 Hx). apply Rmult_le_reg_r with (bpow (- fexp ex)). apply bpow_gt_0. rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r. apply Zceil_ub. pattern ex at 3 ; replace ex with (ex - fexp ex + fexp ex)%Z by ring. rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. assert (Hf: IZR (Zpower beta (ex - fexp ex)) = bpow (ex - fexp ex)). apply IZR_Zpower. lia. rewrite <- Hf. apply IZR_le. apply Zceil_glb. rewrite Hf. unfold Zminus. rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. apply Rlt_le. apply Hx. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop