no goals
x : PartENat
⊢ 0 < ⊤ ↔ 1 ≤ ⊤
simp only [iff_true_iff, le_top, natCast_lt_top, ← @Nat.cast_zero PartENat]
x : PartENat
n : ℕ
⊢ 0 < n ↔ 1 ≤ n
x : PartENat
n : ℕ
⊢ 0 < ↑n ↔ 1 ≤ ↑n
rw [← Nat.cast_zero, ← Nat.cast_one, PartENat.coe_lt_coe, PartENat.coe_le_coe]
no goals
x : PartENat
n : ℕ
⊢ 0 < n ↔ 1 ≤ n
rfl