rw [hi, trunc_next_comm npos, trunc_idempotent npos]
case inr
n : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
x : ℕ
hi : round x = next n (trunc n x)
⊢ trunc n (round x) = round x
no goals