proposition: Theorem FexpGeUnderf: forall e:Z, forall f:float, (Fbounded bo f) -> ((powerRZ radix e) <= Rabs f)%R -> (e-precision+1 <= Fexp f)%Z.
proof: Proof. intros. assert (e < Fexp f+precision)%Z; auto with zarith. apply Zlt_powerRZ with radix;auto with real zarith. apply Rle_lt_trans with (1:=H0). unfold FtoRradix; rewrite <- Fabs_correct; auto. rewrite Zplus_comm; rewrite powerRZ_add; auto with real zarith. unfold Fabs, FtoR; simpl. apply Rmult_lt_compat_r; auto with real zarith. apply powerRZ_lt; try apply IZR_lt; auto with zarith. apply Rlt_le_trans with (Zpos (vNum bo)); auto with zarith real; try apply IZR_lt, H. rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz