proposition: Lemma sqrt_error_N_FLX_aux2 x (Fx : format x) : (1 <= x)%R -> (x = 1 :> R \/ x = 1 + 2 * u_ro :> R \/ 1 + 4 * u_ro <= x)%R.
proof: Proof. intro HxGe1. assert (Pu_ro : (0 <= u_ro)%R); [apply Rmult_le_pos; [lra|apply bpow_ge_0]|]. destruct (Rle_or_lt x 1) as [HxLe1|HxGt1]; [now left; apply Rle_antisym|right]. assert (F1 : format 1); [now apply generic_format_FLX_1|]. assert (H2eps : (2 * u_ro = bpow (-prec + 1))%R). { unfold u_ro; rewrite bpow_plus; field. } assert (HmuGe1p2eps : (1 + 2 * u_ro <= x)%R). { rewrite H2eps, <- succ_FLX_1. now apply succ_le_lt; [now apply FLX_exp_valid| | |]. } destruct (Rle_or_lt x (1 + 2 * u_ro)) as [HxLe1p2eps|HxGt1p2eps]; [now left; apply Rle_antisym|right]. assert (Hulp1p2eps : (ulp beta (FLX_exp prec) (1 + 2 * u_ro) = 2 * u_ro)%R). { destruct (ulp_succ_pos _ _ _ F1 Rlt_0_1) as [Hsucc|Hsucc]. { now rewrite H2eps, <- succ_FLX_1, <- ulp_FLX_1. } exfalso; revert Hsucc; apply Rlt_not_eq. rewrite succ_FLX_1, mag_1, bpow_1, <- H2eps; simpl. apply (Rlt_le_trans _ 2); [apply Rplus_lt_compat_l|]. { unfold u_ro; rewrite <-Rmult_assoc, Rinv_r, Rmult_1_l; [|lra]. change R1 with (bpow 0); apply bpow_lt; lia. } apply IZR_le, Zle_bool_imp_le, radix_prop. } assert (Hsucc1p2eps : (succ beta (FLX_exp prec) (1 + 2 * u_ro) = 1 + 4 * u_ro)%R). { unfold succ; rewrite Rle_bool_true; [rewrite Hulp1p2eps; ring|]. apply Rplus_le_le_0_compat; lra. } rewrite <- Hsucc1p2eps. apply succ_le_lt; [now apply FLX_exp_valid| |exact Fx|now simpl]. rewrite H2eps, <- succ_FLX_1. now apply generic_format_succ; [apply FLX_exp_valid|]. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative Sterbenz Mult_error