proposition: Lemma relative_error_le_conversion_inv : forall x b, (exists eps, (Rabs eps <= b)%R /\ round beta fexp rnd x = (x * (1 + eps))%R) -> (Rabs (round beta fexp rnd x - x) <= b * Rabs x)%R.
proof: Proof. Proof with auto with typeclass_instances. intros x b (eps, (Beps, Heps)). assert (Pb : (0 <= b)%R); [now revert Beps; apply Rle_trans, Rabs_pos|]. rewrite Heps; replace (_ - _)%R with (eps * x)%R; [|ring]. now rewrite Rabs_mult; apply Rmult_le_compat_r; [apply Rabs_pos|]. Qed.
imports: Coq(ZArith Reals Psatz) Core