proposition: Theorem scaled_mantissa_lt_1 : forall x ex, (Rabs x < bpow ex)%R -> (ex <= fexp ex)%Z -> (Rabs (scaled_mantissa x) < 1)%R.
proof: Proof. intros x ex Ex He. destruct (Req_dec x 0) as [Zx|Zx]. rewrite Zx, scaled_mantissa_0, Rabs_R0. now apply IZR_lt. rewrite <- scaled_mantissa_abs. unfold scaled_mantissa. rewrite cexp_abs. unfold cexp. destruct (mag beta x) as (ex', Ex'). simpl. specialize (Ex' Zx). apply (mantissa_small_pos _ _ Ex'). assert (ex' <= fexp ex)%Z. apply Z.le_trans with (2 := He). apply bpow_lt_bpow with beta. now apply Rle_lt_trans with (2 := Ex). now rewrite (proj2 (proj2 (valid_exp _) He)). Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop