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