cases eq_or_ne (trunc n (b - w)) (b - w) with
| inr ne =>
  rewrite [trunc_pred_eq_trunc_of_trunc_ne_self npos ne]
  exact ih
| inl hfb₁ =>
  have bpos : 0 < b - w :=
    Nat.zero_lt_of_lt $ Nat.lt_pred_iff.mp $ Nat.sub_succ _ _ ▸ h
  rewrite [trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq bpos hfb₁]
  rewrite [tsub_right_comm]
  rewrite [trunc_eq_iff_ulp_dvd]
  apply Nat.dvd_sub'
  . calc ulp n (b - w - a - ulp n (b - w - 1))
      _ ∣ ulp n (b - w - a) := ulp_dvd_ulp n tsub_le_self
      _ ∣ b - w - a         := ulp_dvd_of_trunc_eq $ hfb₁ ▸ ih
  . apply ulp_dvd_ulp
    calc b - w - a - ulp n (b - w - 1)
      _ ≤ b - w - a - 1 := tsub_le_tsub_left (Nat.one_le_of_lt $ ulp_pos n _) _
      _ ≤ b - w - 1     := tsub_le_tsub_right tsub_le_self _
case succ
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
⊢ trunc n (trunc n (b - w - 1) - a) = trunc n (b - w - 1) - a
no goals