---

Step * 2 of Lemma posint_is_ufm


WellFnd{i}(|<ℤ+,*>|;x,y.x p| y)
BY
{ ((BLemma `posint_well_fnd`) THEN Auto) }

---

Latex:

---

Latex:

WellFnd\{i\}(|<\mBbbZ{}\msupplus{},*>|;x,y.x  p|  y)


By

---

Latex:
((BLemma  `posint\_well\_fnd`)  THEN  Auto)

---

Home Index