unfold ulp expt
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 x
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ 2 ^ (Nat.size y - n) ≤ 2 ^ (Nat.size x - n)