have ulp_le : ulp n a ≤ 2 * b := by
  have ⟨d, hd⟩ := two_dvd_ulp_of_no_uflow no_uflow
  rewrite [← ulp_eq, hd]
  apply Nat.mul_le_mul_left
  apply Nat.le_of_add_le_add_left (a := a)
  trans trunc n (a + b) + ulp n (a + b) / 2
  . rewrite [hd, Nat.mul_div_cancel_left _ two_pos]
    apply Nat.add_le_add_right
    trans trunc n a
    . exact hfa.ge
    . apply trunc_le_trunc npos
      exact Nat.le_add_right _ _
  . apply midpoint_le_of_round_eq_next_trunc npos hcorrect₁
    exact round_eq_next_trunc_of_gt hfaithful₁ lt_round
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
hfa : trunc n a = a
no_uflow : 2 ^ n ≤ a + b
no_carry : a + b < 2 ^ Nat.size a
lt_round : a + b < round (a + b)
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
ulp_le : ulp n a ≤ 2 * b
⊢ ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b