---

Step * of Lemma mul_preserves_le

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

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

---

Latex:

---

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


By

---

Latex:
TACTIC:(UnivCD  THENA  Auto)

---

Home Index