proposition: Lemma s1p2u_rom1_pos : (0 <= sqrt (1 + 2 * u_ro) - 1)%R.
proof: Proof. apply (Rplus_le_reg_r 1); ring_simplify. 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