proposition: Theorem FulpLeGeneral : forall p : float, Fbounded b p -> (Fulp b radix precision p <= Rabs (FtoRradix p) * powerRZ radix (Z.succ (- precision)) + powerRZ radix (- dExp b))%R.
proof: Proof. intros p Hp. cut (Fcanonic radix b (Fnormalize radix b precision p)); [ intros H | apply FnormalizeCanonic; auto with arith zarith ]. case H; intros H1. apply Rle_trans with (Rabs (FtoR radix p) * powerRZ radix (Z.succ (- precision)))%R. apply FulpLe2; auto with zarith. apply Rle_trans with (Rabs p * powerRZ radix (Z.succ (- precision)) + 0)%R; [ right; fold FtoRradix; ring | apply Rplus_le_compat_l; auto with real zarith ]. now apply powerRZ_le, IZR_lt. apply Rle_trans with (powerRZ radix (- dExp b)). right; unfold Fulp in |- *; simpl in |- *. replace (Fexp (Fnormalize radix b precision p)) with (- dExp b)%Z; [ auto with real zarith | elim H1; intuition ]. apply Rle_trans with (0 + powerRZ radix (- dExp b))%R; [ right; ring | apply Rplus_le_compat_r ]. apply Rmult_le_pos; try apply Rabs_pos. now apply powerRZ_le, IZR_lt. Qed.
imports: Reals ZArith List PeanoNat Psatz