---

Step * 1 1 of Lemma posint_cancel


1. u : ℕ+
2. v : ℕ+
3. w : ℕ+
4. (w * u) = (w * v) ∈ ℕ+
5. u = v ∈ ℤ
⊢ u = v ∈ ℕ+
BY
{ Auto }

---

Latex:

---

Latex:

1.  u  :  \mBbbN{}\msupplus{}
2.  v  :  \mBbbN{}\msupplus{}
3.  w  :  \mBbbN{}\msupplus{}
4.  (w  *  u)  =  (w  *  v)
5.  u  =  v
\mvdash{}  u  =  v


By

---

Latex:
Auto

---

Home Index