proposition: Lemma FloatFexp_gt: forall e f, Fbounded b f -> (bpow beta (e+p) <= Rabs (FtoR beta f))%R -> (e < Pff.Fexp f)%Z.
proof: Proof. intros e f Ff H1. apply lt_bpow with beta. apply Rmult_lt_reg_r with (bpow beta p). apply bpow_gt_0. rewrite <- bpow_plus. apply Rle_lt_trans with (1:=H1). rewrite <- Fabs_correct. 2: apply radix_gt_0. unfold Fabs, FtoR; simpl; rewrite Rmult_comm. rewrite bpow_powerRZ. apply Rmult_lt_compat_l. apply powerRZ_lt. apply IZR_lt, radix_gt_0. destruct Ff as (T1,T2). rewrite bpow_powerRZ. replace p with (Z.of_nat (Z.abs_nat p)). rewrite <- Zpower_nat_Z_powerRZ. apply IZR_lt. now rewrite <- pGivesBound. rewrite inj_abs; lia. Qed.
imports: Coq(Lia) Pff Core