proposition: Theorem ClosestErrorBound : forall (p q : float) (x : R), Fbounded b p -> Closest b radix x p -> q = (x - p)%R :>R -> (Rabs q <= Float 1 (Fexp p) * / 2)%R.
proof: Proof. intros p q x H H0 H1. apply Rle_trans with (Fulp b radix precision p * / 2)%R. rewrite H1. replace (Rabs (x - p)) with (2 * Rabs (x - p) * / 2)%R; [ idtac | field; auto with real ]. apply Rmult_le_compat_r; auto with real. simpl; auto with real. apply ClosestUlp; auto. apply Rmult_le_compat_r. apply Rlt_le. apply Rinv_0_lt_compat; auto with real. unfold FtoRradix in |- *; apply FulpLe; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz