proposition: Theorem round_flx_sqr_sqrt_aux1_simpl: (/ 2 * bpow (mag beta x) + bpow (2+mag beta x - prec) <= (2 * IZR k + 1) * x) -> xk <= z.
proof: Proof. intros H; apply round_flx_sqr_sqrt_aux1. apply Rplus_lt_reg_r with (bpow (2 + mag beta x - prec)). apply Rle_lt_trans with (1:=H). apply Rplus_lt_reg_r with (-(2 * IZR k + 1) * x + (IZR k + / 2) * (IZR k + / 2) * bpow (mag beta x - prec)). apply Rle_lt_trans with (((IZR k + / 2) * (IZR k + / 2) )* bpow (mag beta x - prec)). right; ring. apply Rlt_le_trans with (bpow (2 + mag beta x - prec)). 2: right; ring. unfold Zminus; rewrite <- Zplus_assoc. rewrite bpow_plus with (e1:=2%Z). apply Rmult_lt_compat_r. apply bpow_gt_0. simpl; unfold Z.pow_pos; simpl. rewrite Zmult_1_r, mult_IZR. assert (IZR k + /2 < IZR beta). apply Rle_lt_trans with (IZR (beta -1) + /2). apply Rplus_le_compat_r. apply IZR_le. lia. rewrite minus_IZR; simpl. apply Rplus_lt_reg_r with (-IZR beta + /2). field_simplify. unfold Rdiv; apply Rmult_lt_compat_r. apply Rinv_0_lt_compat, Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. exact Rlt_0_1. assert (0 <= IZR k + / 2). replace 0 with (0+0) by (simpl; ring); apply Rplus_le_compat. apply IZR_le, kpos. apply Rlt_le, Rinv_0_lt_compat, Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. now apply Rmult_le_0_lt_compat. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)