proposition: Lemma u_ro_lt_1 : (u_ro < 1)%R.
proof: Proof. unfold u_ro; apply (Rmult_lt_reg_l 2); [lra|]. rewrite <-Rmult_assoc, Rinv_r, Rmult_1_l, Rmult_1_r; [|lra]. apply (Rle_lt_trans _ (bpow 0)); [apply bpow_le; lia|simpl; lra]. Qed.
imports: Coq(ZArith Reals Psatz) Core