have := calc
  n.succ + (2^length α - 1)
    = n.succ + 2^length α - 1 :=
      by rw [Nat.add_sub_assoc (Nat.pos_pow_of_pos (n:=2) (length α) (by decide))]
  _ = (n + 2^length α).succ - 1 := by rw [Nat.succ_add]
  _ = n + 2^length α := Nat.succ_sub_one ..
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this : 1 % 2 ^ length α = 1
n : Nat
ha : toNat a = Nat.succ n
⊢ Nat.succ n &&& (Nat.succ n + (2 ^ length α - 1)) % 2 ^ length α = Nat.succ n &&& Nat.succ n - 1
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this✝ : 1 % 2 ^ length α = 1
n : Nat
ha : toNat a = Nat.succ n
this : Nat.succ n + (2 ^ length α - 1) = n + 2 ^ length α
⊢ Nat.succ n &&& (Nat.succ n + (2 ^ length α - 1)) % 2 ^ length α = Nat.succ n &&& Nat.succ n - 1