proposition: Theorem round_flx_sqr_sqrt_aux1: (/ 2 * bpow (mag beta x) < (2 * IZR k + 1) * x - (IZR k + / 2) * (IZR k + / 2) * bpow (mag beta x - prec)) -> xk <= z.
proof: Proof. Proof with auto with typeclass_instances. intros V. apply round_N_ge_midp... apply format_xminusk. assert (Z:(mag_val beta xk (mag beta xk) = mag beta x)%Z). apply mag_unique. rewrite Rabs_right; try split. left; now apply xkgt. now apply xklt. apply Rle_ge; left; now apply xkpos. apply Rle_lt_trans with (x - IZR k * ulp_flx x - ulp_flx x / 2). rewrite pred_eq_pos. 2: left; apply xkpos. unfold pred_pos; rewrite Req_bool_false. 2: apply Rgt_not_eq, Rlt_gt. 2: apply Rle_lt_trans with (2:=xkgt). 2: right; apply f_equal, f_equal2... replace (ulp_flx xk) with (ulp_flx x). unfold xk; right; field. rewrite 2!ulp_neq_0; try apply Rgt_not_eq; try assumption. unfold cexp; now rewrite Z. apply xkpos. apply Rle_lt_trans with (x-(IZR k+/2)*ulp_flx x). right; unfold Rdiv; ring. assert (0 <= x - (IZR k + / 2) * ulp_flx x). apply Rplus_le_reg_l with (/2*ulp_flx x). rewrite Rplus_0_r. apply Rle_trans with xk. apply Rle_trans with (1*bpow (mag beta x - 1)). apply Rmult_le_compat. auto with real. apply ulp_ge_0. interval. rewrite ulp_neq_0; try now apply Rgt_not_eq. unfold cexp, FLX_exp. apply bpow_le; lia. rewrite Rmult_1_l. left; apply xkgt. unfold xk; right; ring. rewrite <- (sqrt_square (x - (IZR k + / 2) * ulp_flx x)). 2: assumption. apply sqrt_lt_1_alt. split. apply Rmult_le_pos; assumption. apply Rlt_le_trans with (x*x - /2*bpow (2 * mag beta x - prec)). rewrite ulp_neq_0; try now apply Rgt_not_eq. unfold cexp, FLX_exp. apply Rplus_lt_reg_r with (-x*x). apply Rle_lt_trans with (- (bpow (mag beta x - prec)*((2*IZR k +1)*x - (IZR k + / 2)* (IZR k + / 2) * bpow (mag beta x - prec)))). right; field. apply Rlt_le_trans with (- (bpow (mag beta x - prec)* (/2*bpow (mag beta x)))). apply Ropp_lt_contravar. apply Rmult_lt_compat_l. apply bpow_gt_0. exact V. right; apply trans_eq with ((-/2)*(bpow (mag beta x - prec)*bpow (mag beta x))). ring. rewrite <- bpow_plus. apply trans_eq with ((-/2)*bpow (2 * mag beta x - prec)). apply f_equal. apply f_equal; ring. ring. apply Rplus_le_reg_l with (-y+/2*bpow (2 * mag beta x - prec)). ring_simplify. apply Rle_trans with (-(y-x*x)). right; ring. apply Rle_trans with (1:=RRle_abs _). rewrite Rabs_Ropp. apply Rle_trans with (1:=error_le_half_ulp _ _ _ _)... apply Rmult_le_compat_l. left; auto with real. rewrite ulp_neq_0. 2: apply Rmult_integral_contrapositive_currified; now apply Rgt_not_eq. unfold cexp, FLX_exp. apply bpow_le. apply Zplus_le_compat_r. apply mag_le_bpow. auto with real. rewrite Rabs_mult. replace (2*mag beta x)%Z with (mag beta x+mag beta x)%Z by ring. rewrite bpow_plus. apply Rmult_le_0_lt_compat; try apply Rabs_pos; apply bpow_mag_gt. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)