proposition: Theorem F2R_lt_bpow : forall f : float beta, forall e', (Z.abs (Fnum f) < Zpower beta (e' - Fexp f))%Z -> (Rabs (F2R f) < bpow e')%R.
proof: Proof. intros (m, e) e' Hm. rewrite <- F2R_Zabs. destruct (Zle_or_lt e e') as [He|He]. unfold F2R. simpl. apply Rmult_lt_reg_r with (bpow (-e)). apply bpow_gt_0. rewrite Rmult_assoc, <- 2!bpow_plus, Zplus_opp_r, Rmult_1_r. rewrite <-IZR_Zpower. 2: now apply Zle_left. now apply IZR_lt. elim Zlt_not_le with (1 := Hm). simpl. assert (H: (e' - e < 0)%Z) by lia. clear -H. destruct (e' - e)%Z ; try easy. apply Zabs_pos. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits