proposition: Theorem ClosestExp : forall (p : R) (q : float), Closest b radix p q -> (2 * Rabs (p - q) <= powerRZ radix (Fexp q))%R.
proof: Proof. intros p q H'. apply Rle_trans with (Fulp b radix precision q). apply (ClosestUlp p q); auto. replace (powerRZ radix (Fexp q)) with (FtoRradix (Float 1 (Fexp q))). apply (FulpLe b radix); auto. apply RoundedModeBounded with (radix := radix) (P := Closest b radix) (r := p); auto. apply ClosestRoundedModeP with (precision := precision); auto. unfold FtoRradix, FtoR in |- *; simpl in |- *. ring. Qed.
imports: Reals ZArith List PeanoNat Psatz