apply trunc_eq_trunc_of_le_of_lt npos
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n a = trunc n (a - 1)
case h
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n a ≤ a - 1

case k
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ a - 1 < next n (trunc n a)