---

Step * 1 of Lemma posint_cancel


1. u : ℕ+
2. v : ℕ+
3. w : ℕ+
4. (w * u) = (w * v) ∈ ℕ+
⊢ u = v ∈ ℕ+
BY
{ ((FLemma `mul_cancel_in_eq` [-1]) THENA Auto) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((FLemma  `mul\_cancel\_in\_eq`  [-1])  THENA  Auto)

---

Home Index