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