---

Step * of Lemma q-square-non-neg

∀[q:ℚ]. (0 ≤ (q * q))
BY
{ (Auto THEN BLemma `qmul-non-neg` THEN Auto THEN (RWO "qminus-positive" 0 THENA Auto)) }

1
1. q : ℚ
⊢ (q = 0 ∈ ℚ) ∨ (q = 0 ∈ ℚ) ∨ (0 < q ∧ 0 < q) ∨ (q < 0 ∧ q < 0)

---

Latex:

---

Latex:
\mforall{}[q:\mBbbQ{}].  (0  \mleq{}  (q  *  q))


By

---

Latex:
(Auto  THEN  BLemma  `qmul-non-neg`  THEN  Auto  THEN  (RWO  "qminus-positive"  0  THENA  Auto))

---

Home Index