---

Step * of Lemma rinv1

rinv(r1) = r1
BY
{ (InstLemma `rmul-rinv1` [⌜r1⌝]⋅ THEN Auto) }

1
.....antecedent..... 
rnonzero(r1)

2
1. (r1 * rinv(r1)) = r1
⊢ rinv(r1) = r1

---

Latex:

---

Latex:
rinv(r1)  =  r1


By

---

Latex:
(InstLemma  `rmul-rinv1`  [\mkleeneopen{}r1\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index