---

Step * of Lemma mul_cancel_in_assoced

∀a,b:ℤ. ∀n:ℤ-o.  (((n * a) ~ (n * b)) ⇒ (a ~ b))
BY
{ (Auto THENM (OnMCls [0;-1] (RWH (LemmaC `assoced_elim`)) THENA Auto)) }

1
1. a : ℤ
2. b : ℤ
3. n : ℤ-o
4. ((n * a) = (n * b) ∈ ℤ) ∨ ((n * a) = (-(n * b)) ∈ ℤ)
⊢ (a = b ∈ ℤ) ∨ (a = (-b) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.  \mforall{}n:\mBbbZ{}\msupminus{}\msupzero{}.    (((n  *  a)  \msim{}  (n  *  b))  {}\mRightarrow{}  (a  \msim{}  b))


By

---

Latex:
(Auto  THENM  (OnMCls  [0;-1]  (RWH  (LemmaC  `assoced\_elim`))  THENA  Auto))

---

Home Index