have le_size : n ≤ Nat.size a := by
  rewrite [← Nat.lt_succ, Nat.succ_eq_add_one]
  calc
    n < Nat.size (a + b) := by rwa [Nat.lt_size]
    _ = Nat.size a + 1   := 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
⊢ 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
le_size : n ≤ Nat.size a
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a