conv =>
  rhs; rewrite [← Nat.sub_add_cancel h, Nat.add_comm]
case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo + x % (hi - lo + 1) ≤ hi
case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo + x % (hi - lo + 1) ≤ lo + (hi - lo)