---

Step * of Lemma qmul_preserves_qless

∀[a,b,c:ℚ].  uiff(a < b;c * a < c * b) supposing 0 < c
BY
{ xxxAutoxxx }

1
1. a : ℚ
2. b : ℚ
3. c : ℚ
4. 0 < c
5. a < b
⊢ c * a < c * b

2
1. a : ℚ
2. b : ℚ
3. c : ℚ
4. 0 < c
5. c * a < c * b
⊢ a < b

---

Latex:

---

Latex:
\mforall{}[a,b,c:\mBbbQ{}].    uiff(a  <  b;c  *  a  <  c  *  b)  supposing  0  <  c


By

---

Latex:
xxxAutoxxx

---

Home Index