. rewrite [← tsub_le_iff_right]
  apply tsub_le_tsub_left
  exact Nat.one_le_of_lt (ulp_pos _ _)
case h
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x ≤ trunc n x - 1 + ulp n (trunc n x - 1)

case k
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 + ulp n (trunc n x - 1) < next n (trunc n x)
case k
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 + ulp n (trunc n x - 1) < next n (trunc n x)