apply le_antisymm
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
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
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n y ≤ ulp n (trunc n x)