have : 1 % 2^length α = 1 :=
  Nat.mod_eq_of_lt $ calc
    1 = 2^0 := Eq.symm $ Nat.pow_zero 2
    _ < 2^length α := Nat.pow_lt_pow_right (n:=2) .refl ‹length α > 0›
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
⊢ toNat (UInt.lsb a) = Nat.lsb (toNat a)
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this : 1 % 2 ^ length α = 1
⊢ toNat (UInt.lsb a) = Nat.lsb (toNat a)