apply tsub_le_tsub_right
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ Nat.size y - n ≤ Nat.size x - n
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ Nat.size y ≤ Nat.size x