---

Step * of Lemma mul_preserves_lt

∀[a,b:ℤ]. ∀[n:ℕ+].  n * a < n * b supposing a < b
BY
{ TACTIC:(Auto THEN (All (RWO "less-iff-positive") THENA Auto)) }

1
1. a : ℤ
2. b : ℤ
3. n : ℕ+
4. 0 < b - a
⊢ 0 < (n * b) - n * a

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].  \mforall{}[n:\mBbbN{}\msupplus{}].    n  *  a  <  n  *  b  supposing  a  <  b


By

---

Latex:
TACTIC:(Auto  THEN  (All  (RWO  "less-iff-positive")  THENA  Auto))

---

Home Index