proposition: Theorem scaled_mantissa_lt_bpow : forall x, (Rabs (scaled_mantissa x) < bpow (mag beta x - cexp x))%R.
proof: Proof. intros x. destruct (Req_dec x 0) as [Zx|Zx]. rewrite Zx, scaled_mantissa_0, Rabs_R0. apply bpow_gt_0. apply Rlt_le_trans with (1 := bpow_mag_gt beta _). apply bpow_le. unfold scaled_mantissa. rewrite mag_mult_bpow with (1 := Zx). apply Z.le_refl. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop