1. q : ℚ
2. ¬(q = 0 ∈ ℚ)
3. 0 = (q * q) ∈ ℚ
⊢ 0 < q * q
{ D 2 }
1. q : ℚ
2. 0 = (q * q) ∈ ℚ
⊢ q = 0 ∈ ℚ