have size_eq : Nat.size (a + b) = Nat.size a + 1 := by
  apply Nat.le_antisymm
  . 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 _)
  . rewrite [Nat.succ_le, Nat.lt_size]
    exact carry
n a b : ℕ
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a
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
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a