have : n < length α := hn ▸ Nat.log2RU_lt_self _ ‹length α > 0›
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 : α
this : length α > 0
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < 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 : α
this✝ : length α > 0
this : n < length α
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < length α