proposition: Lemma round_UP_small_pos : forall x ex, (bpow (ex - 1) <= x < bpow ex)%R -> (ex <= fexp ex)%Z -> round Zceil x = (bpow (fexp ex)).
proof: Proof. intros x ex Hx He. rewrite <- F2R_bpow. rewrite <- mantissa_UP_small_pos with (1 := Hx) (2 := He). now rewrite <- cexp_fexp_pos with (1 := Hx). Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop