replace ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a := by
  apply ih
  apply Nat.lt_of_lt_of_le h
  apply tsub_le_tsub_left
  exact Nat.le_succ w
case succ
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
ih : 2 * a < b - w → trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
h : 2 * a < b - Nat.succ w
⊢ trunc n (trunc n (b - Nat.succ w) - a) = trunc n (b - Nat.succ w) - a
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 - Nat.succ w) - a) = trunc n (b - Nat.succ w) - a