simp [bitmask.aux, Nat.not_lt_zero i]
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
hk : Nat.zero ≤ length α
⊢ Nat.getBit 0 i = (decide (i < Nat.zero) && Nat.getBit i (toNat n))
no goals