. rewrite [Nat.size_le, pow_succ, Nat.two_mul]
  apply Nat.add_lt_add
  . exact Nat.lt_size_self _
  . exact Nat.lt_of_le_of_lt hba (Nat.lt_size_self _)
case h₁
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size (a + b) ≤ Nat.size a + 1

case h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size a + 1 ≤ Nat.size (a + b)
case h₂
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ Nat.size a + 1 ≤ Nat.size (a + b)