apply tsub_le_tsub_left
case h
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - ulp n (trunc n x - 1) ≤ trunc n x - 1
case h.h
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ 1 ≤ ulp n (trunc n x - 1)