---

Step * of Lemma posint_div_dec

∀a,b:|<ℤ+,*>|.  Dec(a | b)
BY
{ (RepUR ``grp_car posint_mul_mon mdivides`` 0 THEN Auto) }

1
.....decidable?..... 
1. a : ℕ+
2. b : ℕ+
⊢ Dec(∃c:ℕ+. (b = (a * c) ∈ ℕ+))

---

Latex:

---

Latex:
\mforall{}a,b:|<\mBbbZ{}\msupplus{},*>|.    Dec(a  |  b)


By

---

Latex:
(RepUR  ``grp\_car  posint\_mul\_mon  mdivides``  0  THEN  Auto)

---

Home Index