cases hfaithful₁ x with
| inl lo => rw [lo, trunc_idempotent npos]
| inr hi => rw [hi, trunc_next_comm npos, trunc_idempotent npos]
n : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
x : ℕ
⊢ trunc n (round x) = round x
no goals