---

Step * of Lemma qdiv-int-elim

∀[p:ℤ]. ∀[q:ℤ-o].  ((p/q) ~ <p, q>)
BY
{ ((Auto THEN RepUR ``qdiv qinv qmul`` 0) THEN Repeat ((CallByValueReduce 0 THENA Auto)) THEN (Reduce 0 THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[p:\mBbbZ{}].  \mforall{}[q:\mBbbZ{}\msupminus{}\msupzero{}].    ((p/q)  \msim{}  <p,  q>)


By

---

Latex:
((Auto  THEN  RepUR  ``qdiv  qinv  qmul``  0)
  THEN  Repeat  ((CallByValueReduce  0  THENA  Auto))
  THEN  (Reduce  0  THEN  Auto)\mcdot{})

---

Home Index