rw [eq, round_trunc npos x hfaithful₀]
case inr
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
eq : y = trunc n x
⊢ round y ≤ trunc n x
no goals