exfalso
case inl
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
hlo : round x = trunc n x
⊢ round x = next n (trunc n x)
case inl.h
n x : ℕ
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x > x
hlo : round x = trunc n x
⊢ False