proposition: Lemma error_N_FLT_aux : forall x, (0 < x)%R -> exists eps, exists eta, (Rabs eps <= /2 * bpow (-prec + 1))%R /\ (Rabs eta <= /2 * bpow (emin))%R /\ (eps*eta=0)%R /\ round beta (FLT_exp emin prec) (Znearest choice) x = (x * (1 + eps) + eta)%R.
proof: Proof. intros x Hx2. case (Rle_or_lt (bpow (emin+prec)) x); intros Hx. destruct relative_error_N_ex with (FLT_exp emin prec) (emin+prec)%Z prec choice x as (eps,(Heps1,Heps2)). now apply FLT_exp_valid. intros; unfold FLT_exp. lia. rewrite Rabs_right;[assumption|apply Rle_ge; now left]. exists eps; exists 0%R. split;[assumption|split]. rewrite Rabs_R0; apply Rmult_le_pos. apply Rlt_le, pos_half_prf. apply bpow_ge_0. split;[apply Rmult_0_r|idtac]. now rewrite Rplus_0_r. exists 0%R; exists (round beta (FLT_exp emin prec) (Znearest choice) x - x)%R. split. rewrite Rabs_R0; apply Rmult_le_pos. apply Rlt_le, pos_half_prf. apply bpow_ge_0. split. apply Rle_trans with (/2*ulp beta (FLT_exp emin prec) x)%R. apply error_le_half_ulp. now apply FLT_exp_valid. apply Rmult_le_compat_l. apply Rlt_le, pos_half_prf. rewrite ulp_neq_0. 2: now apply Rgt_not_eq. apply bpow_le. unfold FLT_exp, cexp. rewrite Zmax_right. lia. destruct (mag beta x) as (e,He); simpl. assert (e-1 < emin+prec)%Z. apply (lt_bpow beta). apply Rle_lt_trans with (2:=Hx). rewrite <- (Rabs_pos_eq x) by now apply Rlt_le. now apply He, Rgt_not_eq. lia. split ; ring. Qed.
imports: Coq(ZArith Reals Psatz) Core