---

Step * of Lemma right_mul_preserves_le

∀[a,b:ℤ]. ∀[n:ℕ].  (a * n) ≤ (b * n) supposing a ≤ b
BY
{ (InstLemma `mul_preserves_le` [] THEN RepeatFor 4 (ParallelLast')) }

1
1. a : ℤ
2. b : ℤ
3. n : ℕ
4. a ≤ b
5. (n * a) ≤ (n * b)
⊢ (a * n) ≤ (b * n)

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].  \mforall{}[n:\mBbbN{}].    (a  *  n)  \mleq{}  (b  *  n)  supposing  a  \mleq{}  b


By

---

Latex:
(InstLemma  `mul\_preserves\_le`  []  THEN  RepeatFor  4  (ParallelLast'))

---

Home Index