theorem ENat.mul_eq_top {a b : ℕ∞} : a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0

@[simp]

theorem ENat.le_toNat_self_iff {n : ℕ∞} : n ≤ ↑n.toNat ↔ n ≠ ⊤