---

Step * 1 1 1 1 1 of Lemma sg-inv-op


1. sg : s-Group
2. v : Point
⊢ v ≡ (v v) ⇒ v ≡ 1
BY
{ (Auto THEN (Assert (v v^-1) ≡ ((v v) v^-1) BY (RWO "-1<" 0 THEN Auto))) }

1
1. sg : s-Group
2. v : Point
3. v ≡ (v v)
4. (v v^-1) ≡ ((v v) v^-1)
⊢ v ≡ 1

---

Latex:

---

Latex:

1.  sg  :  s-Group
2.  v  :  Point
\mvdash{}  v  \mequiv{}  (v  v)  {}\mRightarrow{}  v  \mequiv{}  1


By

---

Latex:
(Auto  THEN  (Assert  (v  v\^{}-1)  \mequiv{}  ((v  v)  v\^{}-1)  BY  (RWO  "-1<"  0  THEN  Auto)))

---

Home Index