. rewrite [Nat.div_lt_iff_lt_mul (ulp_pos n x)]
  rewrite [Nat.mul_comm, Nat.mul_succ, Nat.mul_comm]
  rewrite [← trunc, ← ulp_trunc npos, ← next]
  exact k
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x < x / ulp n x + 1
no goals