proposition: Theorem exp_small_round_0_pos : forall x ex, (bpow (ex - 1) <= x < bpow ex)%R -> round x = 0%R -> (ex <= fexp ex)%Z .
proof: Proof. intros x ex H H1. case (Zle_or_lt ex (fexp ex)); trivial; intros V. contradict H1. apply Rgt_not_eq. apply Rlt_le_trans with (bpow (ex-1)). apply bpow_gt_0. apply (round_bounded_large_pos); assumption. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop