---

Step * of Lemma mul_cancel_in_le

∀[a,b:ℤ]. ∀[n:ℕ+].  a ≤ b supposing (n * a) ≤ (n * b)
BY
{ Auto }

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index