have eq_pow : trunc n (a + b) = 2 ^ Nat.size a := by
  have pow_size_eq_pow_mul_ulp : 2 ^ Nat.size a = 2 ^ n * ulp n a := by
    unfold ulp expt
    rewrite [← pow_add]
    rw [add_tsub_cancel_of_le le_size]
  have div_ulp_eq_pow : (a + b) / ulp n a = 2 ^ n := by
    apply Nat.eq_of_mul_eq_mul_right (ulp_pos n a)
    apply div_mul_eq_of_dvd_of_le_of_lt
    . exact Nat.dvd_mul_left _ _
    . exact pow_size_eq_pow_mul_ulp.ge.trans carry
    . apply Nat.lt_of_lt_of_le add_lt_pow_add_ulp
      rw [pow_size_eq_pow_mul_ulp]
  unfold trunc
  rewrite [ulp_eq]
  rewrite [← Nat.mul_assoc]
  rewrite [Nat.mul_comm 2]
  rewrite [← Nat.div_div_eq_div_mul]
  rewrite [div_ulp_eq_pow]
  rewrite [Nat.div_mul_cancel $ dvd_pow_self _ (Nat.not_eq_zero_of_lt npos)]
  exact pow_size_eq_pow_mul_ulp.symm
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
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
eq_pow : trunc n (a + b) = 2 ^ Nat.size a
⊢ round (a + b) ≤ a + b