rw [size_eq]
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a + 1
le_size : n ≤ Nat.size a
⊢ 2 ^ (Nat.size (a + b) - n) = 2 ^ (Nat.size a + 1 - n)
no goals