proposition: Lemma round_N_small_pos : forall x, forall ex, (Raux.bpow beta (ex - 1) <= x < Raux.bpow beta ex)%R -> (ex < fexp ex)%Z -> (round Znearest x = 0)%R.
proof: Proof. intros x ex Hex Hf. unfold round, F2R, scaled_mantissa, cexp; simpl. apply (Rmult_eq_reg_r (bpow (- fexp (mag beta x)))); [|now apply Rgt_not_eq; apply bpow_gt_0]. rewrite Rmult_0_l, Rmult_assoc, <- bpow_plus. replace (_ + - _)%Z with 0%Z by ring; simpl; rewrite Rmult_1_r. apply IZR_eq. apply Znearest_imp. unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r. assert (H : (x >= 0)%R). { apply Rle_ge; apply Rle_trans with (bpow (ex - 1)); [|exact (proj1 Hex)]. now apply bpow_ge_0. } assert (H' : (x * bpow (- fexp (mag beta x)) >= 0)%R). { apply Rle_ge; apply Rmult_le_pos. - now apply Rge_le. - now apply bpow_ge_0. } rewrite Rabs_right; [|exact H']. apply (Rmult_lt_reg_r (bpow (fexp (mag beta x)))); [now apply bpow_gt_0|]. rewrite Rmult_assoc, <- bpow_plus. replace (- _ + _)%Z with 0%Z by ring; simpl; rewrite Rmult_1_r. apply (Rlt_le_trans _ _ _ (proj2 Hex)). apply Rle_trans with (bpow (fexp (mag beta x) - 1)). - apply bpow_le. rewrite (mag_unique beta x ex); [lia|]. now rewrite Rabs_right. - unfold Zminus; rewrite bpow_plus. rewrite Rmult_comm. apply Rmult_le_compat_r; [now apply bpow_ge_0|]. unfold Raux.bpow, Z.pow_pos; simpl. rewrite Zmult_1_r. apply Rinv_le; [exact Rlt_0_2|]. apply IZR_le. destruct beta as (beta_val,beta_prop). now apply Zle_bool_imp_le. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop