apply next_le_next
case inl.a
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
⊢ next n (trunc n y) ≤ next n (trunc n (trunc n x - 1))
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
⊢ trunc n y ≤ trunc n (trunc n x - 1)