proposition: Theorem relative_error_N_FLT_F2R_emin_ex : forall m, let x := F2R (Float beta m emin) in exists eps, (Rabs eps <= /2 * bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) (Znearest choice) x = (x * (1 + eps))%R.
proof: Proof. Proof with auto with typeclass_instances. intros m x. apply relative_error_le_conversion... apply Rmult_le_pos. apply Rlt_le. apply (RinvN_pos 1). apply bpow_ge_0. now apply relative_error_N_FLT_F2R_emin. Qed.
imports: Coq(ZArith Reals Psatz) Core