proposition: Theorem round_bounded_small_pos : forall x ex, (ex <= fexp ex)%Z -> (bpow (ex - 1) <= x < bpow ex)%R -> round x = 0%R \/ round x = bpow (fexp ex).
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. left. apply Rmult_eq_0_compat_r. apply IZR_eq. apply Zfloor_imp. refine (let H := _ in conj (Rlt_le _ _ (proj1 H)) (proj2 H)). now apply mantissa_small_pos. right. pattern (bpow (fexp ex)) at 2 ; rewrite <- Rmult_1_l. apply (f_equal (fun m => (m * bpow (fexp ex))%R)). apply IZR_eq. apply Zceil_imp. refine (let H := _ in conj (proj1 H) (Rlt_le _ _ (proj2 H))). now apply mantissa_small_pos. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop