---

Step * 1 1 of Lemma grp_op_cancel_r


1. g : IGroup
2. a : |g|
3. b : |g|
4. c : |g|
5. ((a * c) * (~ c)) = ((b * c) * (~ c)) ∈ |g|
⊢ a = b ∈ |g|
BY
{ RW  
 (HigherC (RevLemmaC `mon_assoc`) 
  ANDTHENC HigherC (GenLemmaC 1 `grp_inverse`) 
  ANDTHENC HigherC (GenLemmaC 1 `mon_ident`) 
 ) 5 
THEN Auto }

---

Latex:

---

Latex:

1.  g  :  IGroup
2.  a  :  |g|
3.  b  :  |g|
4.  c  :  |g|
5.  ((a  *  c)  *  (\msim{}  c))  =  ((b  *  c)  *  (\msim{}  c))
\mvdash{}  a  =  b


By

---

Latex:
RW   
  (HigherC  (RevLemmaC  `mon\_assoc`) 
    ANDTHENC  HigherC  (GenLemmaC  1  `grp\_inverse`) 
    ANDTHENC  HigherC  (GenLemmaC  1  `mon\_ident`) 
  )  5 
THEN  Auto

---

Home Index