proposition: Lemma relative_error_lt_conversion : forall x b, (0 < b)%R -> (x <> 0 -> Rabs (round beta fexp rnd x - x) < b * Rabs x)%R -> exists eps, (Rabs eps < b)%R /\ round beta fexp rnd x = (x * (1 + eps))%R.
proof: Proof. Proof with auto with typeclass_instances. intros x b Hb0 Hxb. destruct (Req_dec x 0) as [Hx0|Hx0]. exists 0%R. split. now rewrite Rabs_R0. rewrite Hx0, Rmult_0_l. apply round_0... specialize (Hxb Hx0). exists ((round beta fexp rnd x - x) / x)%R. split. 2: now field. unfold Rdiv. rewrite Rabs_mult. apply Rmult_lt_reg_r with (Rabs x). now apply Rabs_pos_lt. rewrite Rmult_assoc, <- Rabs_mult. rewrite Rinv_l with (1 := Hx0). now rewrite Rabs_R1, Rmult_1_r. Qed.
imports: Coq(ZArith Reals Psatz) Core