proposition: Theorem relative_error_FLT_ex : forall x, (bpow (emin + prec - 1) <= Rabs x)%R -> exists eps, (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) rnd x = (x * (1 + eps))%R.
proof: Proof. Proof with auto with typeclass_instances. intros x Hx. apply relative_error_lt_conversion... apply bpow_gt_0. intros _; now apply relative_error_FLT. Qed.
imports: Coq(ZArith Reals Psatz) Core