. apply add_lt_add_of_lt_of_le
  . exact tsub_lt_self xpos zero_lt_one
  . exact ulp_le_ulp n tsub_le_self
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)
no goals