proposition: Theorem F2R_p1_le_bpow : forall m e1 e2 : Z, (0 < m)%Z -> (F2R (Float beta m e1) < bpow e2)%R -> (F2R (Float beta (m + 1) e1) <= bpow e2)%R.
proof: Proof. intros m e1 e2 Hm. intros H. assert (He : (e1 <= e2)%Z). apply (le_bpow beta). apply Rle_trans with (F2R (Float beta m e1)). unfold F2R. simpl. rewrite <- (Rmult_1_l (bpow e1)) at 1. apply Rmult_le_compat_r. apply bpow_ge_0. apply IZR_le. now apply (Zlt_le_succ 0). now apply Rlt_le. revert H. replace e2 with (e2 - e1 + e1)%Z by ring. rewrite bpow_plus. unfold F2R. simpl. rewrite <- (IZR_Zpower beta (e2 - e1)). intros H. apply Rmult_le_compat_r. apply bpow_ge_0. apply Rmult_lt_reg_r in H. apply IZR_le. apply Zlt_le_succ. now apply lt_IZR. apply bpow_gt_0. now apply Zle_minus_le_0. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits