---

Step * 1 1 of Lemma assert-is-qrep

.....wf..... 
1. p : ℤ × ℕ+
2. ↑is-qrep(p)
⊢ p ∈ ℚ
BY
{ xxx(D 1 THEN Fold `mk-rational` 0 THEN Auto)xxx }

---

Latex:

---

Latex:
.....wf..... 
1.  p  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
2.  \muparrow{}is-qrep(p)
\mvdash{}  p  \mmember{}  \mBbbQ{}


By

---

Latex:
xxx(D  1  THEN  Fold  `mk-rational`  0  THEN  Auto)xxx

---

Home Index