. show _ ≤ hi
  conv =>
    rhs; rewrite [← Nat.sub_add_cancel h, Nat.add_comm]
  refine Nat.add_le_add_left ?_ lo
  apply Nat.le_of_lt_succ
  exact x.mod_lt (hi - lo).zero_lt_succ
case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo + x % (hi - lo + 1) ≤ hi
no goals