have ulp_eq : ulp n (a + b) = 2 * ulp n a := by
  calc
    ulp n (a + b)
      = 2 ^ (Nat.size (a + b) - n) := rfl
    _ = 2 ^ (Nat.size a + 1 - n)   := by rw [size_eq]
    _ = 2 ^ (Nat.size a - n + 1)   := by rw [← tsub_add_eq_add_tsub le_size]
    _ = 2 * 2 ^ (Nat.size a - n)   := by rw [pow_succ]
    _ = 2 * ulp n a                := rfl
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
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
ulp_eq : ulp n (a + b) = 2 * ulp n a
⊢ n ≤ Nat.size a ∧ ulp n (a + b) = 2 * ulp n a