. apply Nat.lt_of_lt_of_le add_lt_pow_add_ulp
  rw [pow_size_eq_pow_mul_ulp]
case h₃
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
hba : b ≤ a
no_uflow : 2 ^ n ≤ a + b
carry : 2 ^ Nat.size a ≤ a + b
lt_ulp : b < ulp n (a + b)
le_size : n ≤ Nat.size a
ulp_eq : ulp n (a + b) = 2 * ulp n a
add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a
pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a
⊢ a + b < 2 ^ n * ulp n a + ulp n a
no goals