. rewrite [← Nat.mul_div_cancel (x / ulp n x) (ulp_pos n x)]
  exact Nat.div_le_div_right h
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
⊢ x / ulp n x ≤ y / ulp n x

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
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