have ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2 := by
  have size_lt_size : Nat.size (a - b) < Nat.size a := by
    rewrite [← Nat.succ_pred (Nat.not_eq_zero_of_lt lt_size)]
    rewrite [Nat.lt_succ, ← Nat.sub_one]
    rewrite [Nat.size_le, ← eq_pow]
    exact tsub_lt_self apos bpos
  have pow_lt : 2 ^ (Nat.size a - 1) / 2 < a - b := by
    rewrite [lt_tsub_comm]
    conv => rhs ; left ; rewrite [eq_pow]
    rewrite [sub_half_of_even even]
    apply lt_of_mul_lt_mul_left' (a := 2)
    rewrite [Nat.mul_div_cancel_left' even]
    rewrite [← eq_pow]
    exact two_mul_lt
  have size_eq_size_sub_one : Nat.size (a - b) = Nat.size a - 1 := by
    apply Nat.le_antisymm
    . rewrite [← Nat.lt_iff_le_pred size_pos]
      exact size_lt_size
    . apply Nat.le_of_pred_lt
      rewrite [← Nat.sub_one]
      rewrite [Nat.lt_size]
      rewrite [← Nat.pow_div (Nat.one_le_of_lt size_sub_one_pos) two_pos]
      rewrite [pow_one]
      exact pow_lt.le
  have size_add_one_eq_size : Nat.size (a - b) + 1 = Nat.size a := by
    rewrite [← Nat.succ_pred (Nat.not_eq_zero_of_lt size_pos)]
    rewrite [← Nat.sub_one, ← Nat.add_one]
    apply congr_arg (fun w => w + 1)
    exact size_eq_size_sub_one
  have le_size : n ≤ Nat.size (a - b) := by
    apply Nat.le_of_lt
    rewrite [Nat.lt_size]
    exact no_uflow
  have two_ulp_eq_ulp : 2 * ulp n (a - b) = ulp n a := by
    rewrite [← pow_one 2]
    unfold ulp expt
    rewrite [← pow_add]
    rewrite [Nat.add_comm]
    rewrite [tsub_add_eq_add_tsub le_size]
    apply congr_arg (fun w => 2 ^ (w - n))
    exact size_add_one_eq_size
  have ulp_even' : 2 ∣ ulp n a :=
    Nat.dvd_trans ulp_even $ ulp_dvd_ulp n tsub_le_self
  apply mul_left_cancel₀ two_ne_zero
  rewrite [Nat.mul_div_cancel_left' ulp_even']
  exact two_ulp_eq_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
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
⊢ ulp n (a - b) ≤ 2 * 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
hfb : trunc n b = b
hba : b ≤ a
round_lt : round (a - b) < a - b
no_uflow : a - b ≥ 2 ^ n
ulp_lt_ulp : ulp n (a - b) < ulp n a
two_mul_lt : 2 * b < a
bpos : b > 0
le_ulp : b ≤ ulp n (a - b)
ulp_even : 2 ∣ ulp n (a - b)
lt_ulp : b < ulp n a
lt_size : n < Nat.size a
size_sub_one_pos : 0 < Nat.size a - 1
size_pos : 0 < Nat.size a
apos : 0 < a
eq_pow : a = 2 ^ (Nat.size a - 1)
even : 2 ∣ 2 ^ (Nat.size a - 1)
ulp_eq_half_ulp : ulp n (a - b) = ulp n a / 2
⊢ ulp n (a - b) ≤ 2 * b