rewrite [Nat.succ_le, Nat.lt_size]
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
⊢ 2 ^ Nat.size a ≤ a + b