apply Nat.lt_le_asymm (lt_next_trunc npos x)
case inr.h
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x ≤ x
hhi : round x = next n (trunc n x)
⊢ False
case inr.h
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x ≤ x
hhi : round x = next n (trunc n x)
⊢ next n (trunc n x) ≤ x