proposition: Lemma sqrt_error_N_FLX_aux3 : (u_ro / sqrt (1 + 4 * u_ro) <= 1 - 1 / sqrt (1 + 2 * u_ro))%R.
proof: Proof. assert (Pu_ro : (0 <= u_ro)%R); [apply Rmult_le_pos; [lra|apply bpow_ge_0]|]. unfold Rdiv; apply (Rplus_le_reg_r (/ sqrt (1 + 2 * u_ro))); ring_simplify. apply (Rmult_le_reg_r (sqrt (1 + 4 * u_ro) * sqrt (1 + 2 * u_ro))). { apply Rmult_lt_0_compat; apply sqrt_lt_R0; lra. } field_simplify; [|split; apply Rgt_not_eq, Rlt_gt, sqrt_lt_R0; lra]. try unfold Rdiv; rewrite ?Rinv_1, ?Rmult_1_r. apply Rsqr_incr_0_var; [|now apply Rmult_le_pos; apply sqrt_pos]. rewrite <-sqrt_mult; [|lra|lra]. rewrite Rsqr_sqrt; [|apply Rmult_le_pos; lra]. unfold Rsqr; ring_simplify; unfold pow; rewrite !Rmult_1_r. rewrite !sqrt_def; [|lra|lra]. apply (Rplus_le_reg_r (-u_ro * u_ro - 1 -4 * u_ro - 2 * u_ro ^ 3)). ring_simplify; apply Rsqr_incr_0_var. { unfold Rsqr; ring_simplify. unfold pow; rewrite !Rmult_1_r, !sqrt_def; [|lra|lra]. apply (Rplus_le_reg_r (-32 * u_ro ^ 4 - 24 * u_ro ^ 3 - 4 * u_ro ^ 2)). ring_simplify. replace (_ + _)%R with (((4 * u_ro ^ 2 - 28 * u_ro + 9) * u_ro + 4) * u_ro ^ 3)%R by ring. apply Rmult_le_pos; [|now apply pow_le]. assert (Heps_le_half : (u_ro <= 1 / 2)%R). { unfold u_ro, Rdiv; rewrite Rmult_comm; apply Rmult_le_compat_r; [lra|]. change 1%R with (bpow 0); apply bpow_le; lia. } apply (Rle_trans _ (-8 * u_ro + 4)); [lra|]. apply Rplus_le_compat_r, Rmult_le_compat_r; [apply Pu_ro|]. now assert (H : (0 <= u_ro ^ 2)%R); [apply pow2_ge_0|lra]. } assert (H : (u_ro ^ 3 <= u_ro ^ 2)%R). { unfold pow; rewrite <-!Rmult_assoc, Rmult_1_r. apply Rmult_le_compat_l; [now apply Rmult_le_pos; apply Pu_ro|]. now apply Rlt_le, u_ro_lt_1. } now assert (H' : (0 <= u_ro ^ 2)%R); [apply pow2_ge_0|lra]. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative Sterbenz Mult_error