proposition: Lemma u_rod1pu_ro_le_u_ro : (u_ro / (1 + u_ro) <= u_ro)%R.
proof: Proof. assert (Pu_ro := u_ro_pos). apply (Rmult_le_reg_r (1 + u_ro)); [lra|]. unfold Rdiv; rewrite Rmult_assoc, Rinv_l; [|lra]. assert (0 <= u_ro * u_ro)%R; [apply Rmult_le_pos|]; lra. Qed.
imports: Coq(ZArith Reals Psatz) Core