---

Step * 1 2 of Lemma qmul-negative


1. a : ℚ@i
2. b : ℚ@i
3. 0 < -(a) * b@i
⊢ a * b < 0
BY
{ (QMul ⌜-1⌝ (-1)⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}@i
2.  b  :  \mBbbQ{}@i
3.  0  <  -(a)  *  b@i
\mvdash{}  a  *  b  <  0


By

---

Latex:
(QMul  \mkleeneopen{}-1\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index