apply ulp_le_ulp
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n (trunc n x) ≤ ulp n y
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ trunc n x ≤ y