have : 1 < 2^length α := calc
  1 < 2^1 := by decide
  _ ≤ 2^k.succ := Nat.pow_le_pow_of_le_right (Nat.zero_lt_succ 1) (Nat.succ_le_succ k.zero_le)
  _ ≤ 2^length α := Nat.pow_le_pow_of_le_right (Nat.zero_lt_succ 1) hk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝ : k < 2 ^ length α
this : 2 ^ toNat n < 2 ^ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))