proposition: Theorem round_FTZ_small : forall x : R, (Rabs x < bpow (emin + prec - 1))%R -> round beta FTZ_exp Zrnd_FTZ x = 0%R.
proof: Proof. Proof with auto with typeclass_instances. intros x Hx. destruct (Req_dec x 0) as [Hx0|Hx0]. rewrite Hx0. apply round_0... unfold round, scaled_mantissa, cexp. destruct (mag beta x) as (ex, He). simpl. specialize (He Hx0). unfold Zrnd_FTZ. rewrite Rle_bool_false. apply F2R_0. rewrite Rabs_mult. rewrite (Rabs_pos_eq (bpow (- FTZ_exp ex))). change 1%R with (bpow 0). rewrite <- (Zplus_opp_r (FTZ_exp ex)). rewrite bpow_plus. apply Rmult_lt_compat_r. apply bpow_gt_0. apply Rlt_le_trans with (1 := Hx). apply bpow_le. unfold FTZ_exp. generalize (Zlt_cases (ex - prec) emin). case Zlt_bool. intros _. apply Z.le_refl. intros He'. elim Rlt_not_le with (1 := Hx). apply Rle_trans with (2 := proj1 He). apply bpow_le. lia. apply bpow_ge_0. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp FLX