have add_lt_pow_add_ulp : a + b < 2 ^ Nat.size a + ulp n a := by
  have ulp_le : ulp n a ≤ 2 ^ Nat.size a := by
    unfold ulp expt
    exact Nat.pow_le_pow_of_le_right two_pos tsub_le_self
  rewrite [← tsub_add_cancel_of_le ulp_le]
  rewrite [Nat.add_assoc]
  rewrite [← Nat.two_mul]
  rewrite [← ulp_eq]
  apply add_lt_add_of_le_of_lt
  . exact le_size_sub_ulp_of_trunc_eq npos hfa
  . exact lt_ulp
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
⊢ round (a + b) ≤ a + b
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
⊢ round (a + b) ≤ a + b