proposition: Lemma om1ds1p2u_ro_le_u_rod1pu_ro : (1 - 1 / sqrt (1 + 2 * u_ro) <= u_ro / (1 + u_ro))%R.
proof: Proof. assert (Pu_ro := u_ro_pos beta prec). apply (Rmult_le_reg_r (sqrt (1 + 2 * u_ro) * (1 + u_ro))). { apply Rmult_lt_0_compat; [apply sqrt_lt_R0|]; lra. } field_simplify; [|lra|intro H; apply sqrt_eq_0 in H; lra]. try unfold Rdiv; unfold Rminus; rewrite ?Rinv_1, ?Rmult_1_r, !Rplus_assoc. rewrite <-(Rplus_0_r (sqrt _ * _)) at 2; apply Rplus_le_compat_l. apply (Rplus_le_reg_r (1 + u_ro)); ring_simplify. rewrite <-(sqrt_square (_ + 1)); [|lra]; apply sqrt_le_1_alt. assert (H : (0 <= u_ro * u_ro)%R); [apply Rmult_le_pos|]; lra. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative Sterbenz Mult_error