proposition: Theorem cexp_FLT_FIX : forall x, x <> 0%R -> (Rabs x < bpow (emin + prec))%R -> cexp beta FLT_exp x = cexp beta (FIX_exp emin) x.
proof: Proof. intros x Hx0 Hx. unfold cexp. apply Zmax_right. unfold FIX_exp. destruct (mag beta x) as (ex, Hex). simpl. cut (ex - 1 < emin + prec)%Z. lia. apply (lt_bpow beta). apply Rle_lt_trans with (2 := Hx). now apply Hex. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE