proposition: Lemma round_flx_sqr_sqrt_snd_deg: (((radix_val beta=5)%Z /\ (3 < prec)%Z) \/ (5 < radix_val beta)%Z) -> sqrt (IZR beta) + / 4 * bpow (3 - prec) <= IZR beta * (2 - bpow (1 - prec)) / (2 * (2 + bpow (1 - prec))).
proof: Proof. intros H; destruct H. destruct H as (H1,H2). apply Rle_trans with (sqrt (IZR beta) + / (4 *IZR beta)). apply Rplus_le_compat_l. rewrite (Rinv_mult_distr 4). apply Rmult_le_compat_l. apply Rlt_le, Rinv_0_lt_compat, Rmult_lt_0_compat; apply Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. apply Rle_trans with (bpow (-(1))). apply bpow_le; lia. right; rewrite bpow_opp. apply f_equal, bpow_1. apply Rgt_not_eq, Rmult_lt_0_compat; apply Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. apply Rgt_not_eq, radix_pos. apply Rle_trans with (IZR beta * (2-/(IZR beta*IZR beta)) / (2* (2 + /(IZR beta*IZR beta)))). rewrite H1;simpl; interval. unfold Rdiv; rewrite 2!Rmult_assoc. apply Rmult_le_compat_l. left; apply radix_pos. apply Rmult_le_compat. rewrite H1; simpl; interval. rewrite H1; simpl; interval. apply Rplus_le_reg_l with (-2); ring_simplify. apply Ropp_le_contravar. apply Rle_trans with (bpow (-(2))). apply bpow_le; lia. right; rewrite bpow_opp. apply f_equal; simpl; unfold Z.pow_pos; simpl. rewrite <- mult_IZR; apply f_equal; ring. apply Rinv_le. apply Rmult_lt_0_compat. apply Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. apply Rplus_lt_0_compat. now apply IZR_lt. apply bpow_gt_0. apply Rmult_le_compat_l. apply Rlt_le,Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. apply Rplus_le_compat_l. apply Rle_trans with (bpow (-(2))). apply bpow_le; lia. right; rewrite bpow_opp. apply f_equal; simpl; unfold Z.pow_pos; simpl. rewrite <- mult_IZR; apply f_equal; ring. apply Rle_trans with (sqrt (IZR beta) + /4*1). apply Rplus_le_compat_l. apply Rmult_le_compat_l. apply Rlt_le, Rinv_0_lt_compat, Rmult_lt_0_compat; apply Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. apply Rle_trans with (bpow 0). apply bpow_le; lia. right; reflexivity. rewrite Rmult_1_r. assert (6 <= IZR beta). apply IZR_le; lia. apply Rle_trans with (IZR beta*(12/25)). apply Rplus_le_reg_l with (-sqrt (IZR beta)); ring_simplify. apply Rle_trans with (IZR beta*(12/25-/sqrt(IZR beta))). apply Rle_trans with (IZR beta*(71/1000)). apply Rle_trans with (IZR 6*(71/1000)). simpl; interval. apply Rmult_le_compat_r. interval. apply IZR_le; lia. apply Rmult_le_compat_l. left; apply radix_pos. interval with (i_prec 30). assert (sqrt (IZR beta) <> 0). apply Rgt_not_eq. apply sqrt_lt_R0, radix_pos. apply Rplus_le_reg_l with (-12/25*IZR beta). unfold Rdiv; ring_simplify. right; rewrite Ropp_mult_distr_l_reverse; apply f_equal. apply Rmult_eq_reg_l with (sqrt (IZR beta)); trivial. apply trans_eq with (IZR beta). field; trivial. apply sym_eq, sqrt_sqrt. left; apply radix_pos. unfold Rdiv; rewrite (Rmult_assoc _ (2 - bpow (1 - prec))). apply Rmult_le_compat_l. left; apply radix_pos. assert (0 <= bpow (1-prec) <= 1/32). split. apply bpow_ge_0. apply Rle_trans with (bpow (-(2))). apply bpow_le. lia. rewrite bpow_opp. simpl; unfold Z.pow_pos; simpl. rewrite Zmult_1_r. apply Rle_trans with (/IZR (6*6)). apply Rinv_le. simpl; interval. apply IZR_le. apply Zmult_le_compat; lia. simpl; interval. interval. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)