rewrite [← size_trunc_eq_size npos y] at size_lt_size
case inl
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_lt_size : Nat.size (trunc n x) < Nat.size y
⊢ trunc n x ≤ trunc n y
case inl
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_lt_size : Nat.size (trunc n x) < Nat.size (trunc n y)
⊢ trunc n x ≤ trunc n y