---

Step * 1 2 1 1 of Lemma rat-int-part_wf

.....equality..... 
1. z1 : ℤ
2. z2 : ℤ-o
⊢ <z1, z2> ~ (z1/z2)
BY
{ (RepUR ``qdiv qmul qinv`` 0 THEN RepeatFor 3 (((CallByValueReduce 0 THEN Reduce 0) THENA Auto)) THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  z1  :  \mBbbZ{}
2.  z2  :  \mBbbZ{}\msupminus{}\msupzero{}
\mvdash{}  <z1,  z2>  \msim{}  (z1/z2)


By

---

Latex:
(RepUR  ``qdiv  qmul  qinv``  0
  THEN  RepeatFor  3  (((CallByValueReduce  0  THEN  Reduce  0)  THENA  Auto))
  THEN  Auto)

---

Home Index