---

Step * 5 of Lemma posint_is_ufm


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index