proposition: Theorem round_flx_sqr_sqrt_aux2: forall n, (0 <= n)%Z -> (2*IZR n * bpow (prec-1) * ulp_flx x * (1+bpow (1-prec)/2) < x) -> round_flx3(x/(x-IZR n*ulp_flx x)) <= 1.
proof: Proof. Proof with auto with typeclass_instances. intros n Hnp Hn. apply round_N_le_midp... replace 1 with (bpow 0) by reflexivity. apply generic_format_bpow. unfold FLX_exp; lia. assert (0 < x - IZR n*ulp_flx x). apply Rplus_lt_reg_r with (IZR n*ulp_flx x); ring_simplify. apply Rle_lt_trans with (2:=Hn). apply Rle_trans with (IZR n*(ulp_flx x*((1*1)*(1+0))));[right; ring|idtac]. apply Rle_trans with (IZR n*(ulp_flx x*(2*bpow (prec - 1)* (1 + bpow (1 - prec) / 2))));[idtac|right; ring]. apply Rmult_le_compat_l. now apply IZR_le. apply Rmult_le_compat_l. unfold ulp; apply ulp_ge_0. apply Rmult_le_compat. rewrite Rmult_1_l; apply Rle_0_1. rewrite Rplus_0_r; apply Rle_0_1. apply Rmult_le_compat; try apply Rle_0_1. auto with real. replace 1 with (bpow 0) by reflexivity. apply bpow_le. lia. apply Rplus_le_compat_l. unfold Rdiv; apply Rmult_le_pos. apply bpow_ge_0. auto with real. apply Rmult_lt_reg_r with (x - IZR n*ulp_flx x). assumption. unfold Rdiv; rewrite Rmult_assoc. rewrite Rinv_l. rewrite Rmult_1_r. 2: auto with real. apply Rplus_lt_reg_r with (-x+IZR n*ulp_flx x + IZR n*ulp_flx x* ulp_flx 1 * / 2); ring_simplify. apply Rmult_lt_reg_l with (2*/ulp_flx 1). apply Rmult_lt_0_compat. auto with real. apply Rinv_0_lt_compat. rewrite ulp_neq_0; try apply bpow_gt_0. apply Rgt_not_eq, Rlt_0_1. apply Rlt_le_trans with x. apply Rle_lt_trans with (2:=Hn). replace (ulp_flx 1) with (bpow (1-prec)). rewrite <- bpow_opp. replace ((-(1-prec)))%Z with (prec -1)%Z by ring. right; unfold Rdiv; ring. replace 1 with (bpow 0) by reflexivity. rewrite ulp_bpow. apply f_equal; unfold FLX_exp; lia. rewrite succ_eq_pos. right; field. apply Rgt_not_eq. rewrite ulp_neq_0; try apply bpow_gt_0. apply Rgt_not_eq, Rlt_0_1. apply Rle_0_1. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)