---

Step * 4 of Lemma posint_is_ufm


1. a : |<ℤ+,*>|@i
⊢ Dec(Reducible(a))
BY
{ ((BLemma `posint_reduc_dec`) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  |<\mBbbZ{}\msupplus{},*>|@i
\mvdash{}  Dec(Reducible(a))


By

---

Latex:
((BLemma  `posint\_reduc\_dec`)  THEN  Auto)

---

Home Index