case inl h =>
  have : toNat a + 1 < 2^length α := h
  have : 2^length α - (toNat a + 1) < 2^length α :=
    Nat.sub_lt_self (Nat.zero_lt_succ _) (toNat_lt a)
  rw [
    Nat.mod_eq_of_lt ‹toNat a + 1 < 2^length α›,
    Nat.mod_eq_of_lt ‹2^length α - (toNat a + 1) < 2^length α›
  ]
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) < 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
no goals