---

Step * of Lemma div-self

∀[y:ℤ-o]. (y ÷ y ~ 1)
BY
{ ((D 0 THENA Auto)
   THEN (InstLemma `div-cancel` [⌜1⌝;⌜y⌝]⋅ THENA Auto)
   THEN NthHypSq (-1)
   THEN RepeatFor 2 (EqCD)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[y:\mBbbZ{}\msupminus{}\msupzero{}].  (y  \mdiv{}  y  \msim{}  1)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (InstLemma  `div-cancel`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  NthHypSq  (-1)
  THEN  RepeatFor  2  (EqCD)
  THEN  Auto)

---

Home Index