---

Step * of Lemma non-neg-qmul

∀[a,b:ℚ].  (0 ≤ (a * b)) supposing ((0 ≤ b) and (0 ≤ a))
BY
{ xxx(Auto THEN RepeatFor 2 (MoveToConcl (-1)))xxx }

1
1. a : ℚ
2. b : ℚ
⊢ (0 ≤ a) ⇒ (0 ≤ b) ⇒ (0 ≤ (a * b))

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbQ{}].    (0  \mleq{}  (a  *  b))  supposing  ((0  \mleq{}  b)  and  (0  \mleq{}  a))


By

---

Latex:
xxx(Auto  THEN  RepeatFor  2  (MoveToConcl  (-1)))xxx

---

Home Index