cases h
α : 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 α
this✝ : (k >>> toNat n &&& 1) <<< k < 2 ^ length α
this : 0 = i - k ↔ i ≤ k
h : i = k
⊢ i ≥ k ∧ i ≤ k
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
this✝³ : 2 ^ toNat n < 2 ^ length α
this✝² : 1 < 2 ^ length α
h_ind : i ≤ length α → UInt.getBit (bitmask.aux n i) i = (decide (i < i) && Nat.getBit i (toNat n))
hk : Nat.succ i ≤ length α
this✝¹ : i < 2 ^ length α
this✝ : (i >>> toNat n &&& 1) <<< i < 2 ^ length α
this : 0 = i - i ↔ i ≤ i
⊢ i ≥ i ∧ i ≤ i