proposition: Theorem bpow_le_F2R_m1 : forall m e1 e2 : Z, (1 < m)%Z -> (bpow e2 < F2R (Float beta m e1))%R -> (bpow e2 <= F2R (Float beta (m - 1) e1))%R.
proof: Proof. intros m e1 e2 Hm. case (Zle_or_lt e1 e2); intros He. 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. rewrite (Zpred_succ (Zpower _ _)). apply Zplus_le_compat_r. apply Zlt_le_succ. now apply lt_IZR. apply bpow_gt_0. now apply Zle_minus_le_0. intros H. apply Rle_trans with (1*bpow e1)%R. rewrite Rmult_1_l. apply bpow_le. now apply Zlt_le_weak. unfold F2R. simpl. apply Rmult_le_compat_r. apply bpow_ge_0. apply IZR_le. lia. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits