proposition: Lemma om1ds1p2u_ro_pos : (0 <= 1 - 1 / sqrt (1 + 2 * u_ro))%R.
proof: Proof. unfold Rdiv; rewrite Rmult_1_l, <-Rinv_1 at 1. apply Rle_0_minus, Rinv_le; [lra|]. rewrite <- sqrt_1 at 1; apply sqrt_le_1_alt. assert (H := u_ro_pos beta prec); lra. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative Sterbenz Mult_error