---

Step * of Lemma rdiv-self

∀[x:ℝ]. (x/x) = r1 supposing x ≠ r0
BY
{ (Unfold `rdiv` 0 THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (x/x)  =  r1  supposing  x  \mneq{}  r0


By

---

Latex:
(Unfold  `rdiv`  0  THEN  EAuto  1)

---

Home Index