apply Nat.lt_le_asymm h
case inl.h
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
hlo : round x = trunc n x
⊢ False
case inl.h
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
hlo : round x = trunc n x
⊢ round x ≤ x