n : ℕ
this : 0 < size n ↔ 0 < n
⊢ size n = 0 ↔ n = 0
n : ℕ
⊢ size n = 0 ↔ n = 0
have := @size_pos n
n : ℕ
this : ¬size n = 0 ↔ ¬n = 0
⊢ size n = 0 ↔ n = 0
n : ℕ
this : 0 < size n ↔ 0 < n
⊢ size n = 0 ↔ n = 0
simp [pos_iff_ne_zero] at this
no goals
n : ℕ
this : ¬size n = 0 ↔ ¬n = 0
⊢ size n = 0 ↔ n = 0
exact Decidable.not_iff_not.1 this