cases hfaithful₁ x with
| inl hlo => exact hlo
| inr hhi =>
  exfalso
  apply Nat.lt_le_asymm (lt_next_trunc npos x)
  exact hhi ▸ h
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x ≤ x
⊢ round x = trunc n x
no goals