proposition: Theorem relative_error_F2R_emin : forall m, let x := F2R (Float beta m emin) in (x <> 0)%R -> (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs x)%R.
proof: Proof. intros m x Hx. apply relative_error. unfold x. rewrite <- F2R_Zabs. apply bpow_le_F2R. apply lt_F2R with beta emin. rewrite F2R_0, F2R_Zabs. now apply Rabs_pos_lt. Qed.
imports: Coq(ZArith Reals Psatz) Core