---

Step * of Lemma posint_cancel

Cancel(|<ℤ+,*>|;|<ℤ+,*>|;*)
BY
{ (((Unfold `cancel` 0  THEN AbReduce 0  THEN RepD) THENA Auto) THEN Try (((BLemma `mul_bounds_1b`) THEN Auto))) }

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

---

Latex:

---

Latex:
Cancel(|<\mBbbZ{}\msupplus{},*>|;|<\mBbbZ{}\msupplus{},*>|;*)


By

---

Latex:
(((Unfold  `cancel`  0 
  THEN  AbReduce  0 
  THEN  RepD)  THENA  Auto)
  THEN  Try  (((BLemma  `mul\_bounds\_1b`)  THEN  Auto))
  )

---

Home Index