---

Step * of Lemma one-rdiv-rmul

∀[x,y:ℝ].  ((r1/y) * x) = (x/y) supposing y ≠ r0
BY
{ (Auto THEN nRMul ⌜y⌝ 0⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  nRMul  \mkleeneopen{}y\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index