proposition: Theorem ClosestErrorBoundNormal : forall (x : R) (p : float), Closest b radix x p -> Fnormal radix b (Fnormalize radix b precision p) -> (Rabs (x - p) <= Rabs p * (/ 2 * powerRZ radix (Z.succ (- precision))))%R.
proof: Proof. intros x p H H1. apply Rle_trans with (Rabs (FtoRradix p) * (/ 2 * (radix * / Zpos (vNum b))))%R; [ apply ClosestErrorBoundNormal_aux; auto | right ]. replace (powerRZ radix (Z.succ (- precision))) with (radix * / Zpos (vNum b))%R; auto with real. rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ. rewrite Rinv_powerRZ; auto with real zarith. rewrite powerRZ_Zs; auto with real zarith. apply IZR_neq; lia. apply IZR_neq; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz