simp only [if_neg (Nat.not_lt_of_le h)]
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
⊢ lo ≤
      (if lo > hi then hi else lo) +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) * 1000) (0, g)).fst %
          (((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) ∧
    (if lo > hi then hi else lo) +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) * 1000) (0, g)).fst %
          (((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) ≤
      hi
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
⊢ lo ≤
      lo +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((hi - lo + 1) * 1000) (0, g)).fst %
          (hi - lo + 1) ∧
    lo +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((hi - lo + 1) * 1000) (0, g)).fst %
          (hi - lo + 1) ≤
      hi