apply Nat.le_pred_of_lt
case inl.a.h
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ y ≤ trunc n x - 1
case inl.a.h.h
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ y < Nat.sub (trunc n x) 0