proposition: Lemma relative_error_N_round_ex_derive : forall x rx, (exists eps, (Rabs eps <= u_ro / (1 + u_ro))%R /\ rx = (x * (1 + eps))%R) -> exists eps, (Rabs eps <= u_ro)%R /\ x = (rx * (1 + eps))%R.
proof: Proof. intros x rx (d, (Bd, Hd)). assert (Pu_ro := u_ro_pos). assert (H := Rabs_le_inv _ _ Bd). assert (H' := u_rod1pu_ro_le_u_ro); assert (H'' := u_ro_lt_1). destruct (Req_dec rx 0) as [Zfx|Nzfx]. { exists 0%R; split; [now rewrite Rabs_R0|]. rewrite Rplus_0_r, Rmult_1_r, Zfx. now rewrite Zfx in Hd; destruct (Rmult_integral _ _ (sym_eq Hd)); [|lra]. } destruct (Req_dec x 0) as [Zx|Nzx]. { now exfalso; revert Hd; rewrite Zx, Rmult_0_l. } set (d' := ((x - rx) / rx)%R). assert (Hd' : (Rabs d' <= u_ro)%R). { unfold d'; rewrite Hd. replace (_ / _)%R with (- d / (1 + d))%R; [|now field; split; lra]. unfold Rdiv; rewrite Rabs_mult, Rabs_Ropp. rewrite (Rabs_pos_eq (/ _)); [|apply Rlt_le, Rinv_0_lt_compat; lra]. apply (Rmult_le_reg_r (1 + d)); [lra|]. rewrite Rmult_assoc, Rinv_l, Rmult_1_r; [|lra]. apply (Rle_trans _ _ _ Bd). unfold Rdiv; apply Rmult_le_compat_l; [now apply u_ro_pos|]. apply (Rle_trans _ (1 - u_ro / (1 + u_ro))); [right; field|]; lra. } now exists d'; split; [|unfold d'; field]. Qed.
imports: Coq(ZArith Reals Psatz) Core