proposition: Theorem FulpGe : forall p : float, Fbounded b p -> (Rabs p <= (powerRZ radix precision - 1) * Fulp p)%R.
proof: Proof. intros p H. replace (FtoRradix p) with (FtoRradix (Fnormalize radix b precision p)); [ idtac | unfold FtoRradix in |- *; apply FnormalizeCorrect; auto ]. unfold FtoRradix in |- *; rewrite <- Fabs_correct; auto with arith real. unfold FtoR in |- *; simpl in |- *; unfold Fulp in |- *. apply Rmult_le_compat_r; [ apply powerRZ_le, IZR_lt | idtac ]; auto with real arith zarith. apply Rle_trans with (IZR (Z.pred (Zpos (vNum b)))); [ apply IZR_le; auto with zarith | idtac ]. apply Zle_Zpred. apply FnormalizeBounded; auto with zarith. unfold Z.pred in |- *; right; rewrite pGivesBound; replace 1%R with (IZR 1); auto with real. rewrite <- Zpower_nat_Z_powerRZ; rewrite Z_R_minus;auto. Qed.
imports: Reals ZArith List PeanoNat Psatz