have pos := Nat.zero_lt_of_lt lt
case inl
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
⊢ round y ≤ trunc n x
case inl
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
⊢ round y ≤ trunc n x