proposition: Theorem cexp_FLT_FLX : forall x, (bpow (emin + prec - 1) <= Rabs x)%R -> cexp beta FLT_exp x = cexp beta (FLX_exp prec) x.
proof: Proof. intros x Hx. assert (Hx0: x <> 0%R). intros H1; rewrite H1, Rabs_R0 in Hx. contradict Hx; apply Rlt_not_le, bpow_gt_0. unfold cexp. apply Zmax_left. destruct (mag beta x) as (ex, He). unfold FLX_exp. simpl. specialize (He Hx0). cut (emin + prec - 1 < ex)%Z. lia. apply (lt_bpow beta). apply Rle_lt_trans with (1 := Hx). apply He. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE