---

Step * 1 of Lemma sg-inv-unique


1. sg : s-Group
2. x : Point
3. y : Point
4. (x y) ≡ 1
⊢ x^-1 ≡ y
BY
{ ((Assert (x^-1 (x y)) ≡ (x^-1 1) BY (RWO  "-1" 0 THEN Auto)) THEN (RWO "sg-assoc" (-1) THENA Auto)) }

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

---

Latex:

---

Latex:

1.  sg  :  s-Group
2.  x  :  Point
3.  y  :  Point
4.  (x  y)  \mequiv{}  1
\mvdash{}  x\^{}-1  \mequiv{}  y


By

---

Latex:
((Assert  (x\^{}-1  (x  y))  \mequiv{}  (x\^{}-1  1)  BY  (RWO    "-1"  0  THEN  Auto))  THEN  (RWO  "sg-assoc"  (-1)  THENA  Auto))

---

Home Index