proposition: Theorem round_FTZ_FLX : forall x : R, (bpow (emin + prec - 1) <= Rabs x)%R -> round beta FTZ_exp Zrnd_FTZ x = round beta (FLX_exp prec) rnd x.
proof: Proof. intros x Hx. unfold round, scaled_mantissa, cexp. destruct (mag beta x) as (ex, He). simpl. assert (Hx0: x <> 0%R). intros Hx0. apply Rle_not_lt with (1 := Hx). rewrite Hx0, Rabs_R0. apply bpow_gt_0. specialize (He Hx0). assert (He': (emin + prec <= ex)%Z). apply (bpow_lt_bpow beta). apply Rle_lt_trans with (1 := Hx). apply He. replace (FTZ_exp ex) with (FLX_exp prec ex). unfold Zrnd_FTZ. rewrite Rle_bool_true. apply refl_equal. rewrite Rabs_mult. rewrite (Rabs_pos_eq (bpow (- FLX_exp prec ex))). change 1%R with (bpow 0). rewrite <- (Zplus_opp_r (FLX_exp prec ex)). rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. apply Rle_trans with (2 := proj1 He). apply bpow_le. unfold FLX_exp. generalize (prec_gt_0 prec). clear -He' ; lia. apply bpow_ge_0. unfold FLX_exp, FTZ_exp. rewrite Zlt_bool_false. apply refl_equal. clear -He' ; lia. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp FLX