proposition: Lemma round_large_pos_ge_bpow : forall x e, (0 < round rnd x)%R -> (bpow e <= x)%R -> (bpow e <= round rnd x)%R.
proof: Proof. intros x e Hd Hex. destruct (mag beta x) as (ex, He). assert (Hx: (0 < x)%R). apply Rlt_le_trans with (2 := Hex). apply bpow_gt_0. specialize (He (Rgt_not_eq _ _ Hx)). rewrite Rabs_pos_eq in He. 2: now apply Rlt_le. apply Rle_trans with (bpow (ex - 1)). apply bpow_le. cut (e < ex)%Z. lia. apply (lt_bpow beta). now apply Rle_lt_trans with (2 := proj2 He). destruct (Zle_or_lt ex (fexp ex)). destruct (round_bounded_small_pos rnd x ex H He) as [Hr|Hr]. rewrite Hr in Hd. elim Rlt_irrefl with (1 := Hd). rewrite Hr. apply bpow_le. lia. apply (round_bounded_large_pos rnd x ex H He). Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop