proposition: Theorem exp_small_round_0 : forall rnd {Hr : Valid_rnd rnd} x ex, (bpow (ex - 1) <= Rabs x < bpow ex)%R -> round rnd x = 0%R -> (ex <= fexp ex)%Z .
proof: Proof. intros rnd Hr x ex H1 H2. generalize Rabs_R0. rewrite <- H2 at 1. apply (round_abs_abs (fun t rt => forall (ex : Z), (bpow (ex - 1) <= t < bpow ex)%R -> rt = 0%R -> (ex <= fexp ex)%Z)); trivial. clear; intros rnd Hr x Hx. now apply exp_small_round_0_pos. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop