---

Step * 1 1 of Lemma grp_op_cancel_l


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

1
1. g : IGroup
2. a : |g|
3. b : |g|
4. c : |g|
5. b = c ∈ |g|
⊢ b = c ∈ |g|

---

Latex:

---

Latex:

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


By

---

Latex:
RW   
  (HigherC  (LemmaC  `mon\_assoc`) 
    ANDTHENC  HigherC  (GenLemmaC  2  `grp\_inverse`) 
    ANDTHENC  HigherC  (GenLemmaC  2  `mon\_ident`) 
  )  5 
THENA  Auto

---

Home Index