cases Nat.le_total x (trunc n y) with
| inl hxy => exact trunc_le_trunc npos (Nat.le_trans hxy (trunc_le n y))
| inr hyx => exact ge_of_eq (trunc_eq_trunc_of_le_of_lt npos hyx h)
n x y : ℕ
npos : 0 < n
h : x < next n (trunc n y)
⊢ trunc n x ≤ trunc n y
no goals