. simp only [UInt.toNat_ofNat, UInt.toNat_ofNat 1]
  have : length α > 0 :=
    hn |> (length α).rec (λ (hn : 0 = n) => nomatch (trans h hn.symm)) (λ l _ _ => l.zero_lt_succ)
  have : n < length α := hn ▸ Nat.log2RU_lt_self _ ‹length α > 0›
  have : n < 2^length α := trans this (Nat.exp_lt_pow (length α) .refl)
  rw [
      Nat.mod_eq_of_lt (trans h this),
      Nat.mod_eq_of_lt (trans (trans (Nat.le_add_left 1 i) h) this)
  ]
  exact trans (r:=LE.le) (h : i+2 ≤ n) ‹n < length α›
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
⊢ toNat (OfNat.ofNat (i + 1)) + toNat 1 < length α
no goals