proposition: Theorem mantissa_small_pos : forall x ex, (bpow (ex - 1) <= x < bpow ex)%R -> (ex <= fexp ex)%Z -> (0 < x * bpow (- fexp ex) < 1)%R.
proof: Proof. intros x ex Hx He. split. apply Rmult_lt_0_compat. apply Rlt_le_trans with (2 := proj1 Hx). apply bpow_gt_0. apply bpow_gt_0. apply Rmult_lt_reg_r with (bpow (fexp ex)). apply bpow_gt_0. rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_l. rewrite Rmult_1_r, Rmult_1_l. apply Rlt_le_trans with (1 := proj2 Hx). now apply bpow_le. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop