x y : ℕ∞
⊢ ↑withTopEquiv (↑withTopEquiv.symm x) < ↑withTopEquiv (↑withTopEquiv.symm y) ↔ x < y
x y : ℕ∞
⊢ ↑withTopEquiv.symm x < ↑withTopEquiv.symm y ↔ x < y
rw [← withTopEquiv_lt]
no goals
x y : ℕ∞
⊢ ↑withTopEquiv (↑withTopEquiv.symm x) < ↑withTopEquiv (↑withTopEquiv.symm y) ↔ x < y
simp