---

Step * 1 of Lemma massoc_imp_unit_diff


1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. a : |g|
4. b : |g|
5. a ~ b
⊢ ∃u:|g|. ((g-unit(u)) c∧ (a = (u * b) ∈ |g|))
BY
{ Unfold `cancel` 2 THEN Unfold `massoc` 5 }

1
1. g : IAbMonoid
2. ∀[u,v,w:|g|].  u = v ∈ |g| supposing (w * u) = (w * v) ∈ |g|
3. a : |g|
4. b : |g|
5. Symmetrize(x,y.x | y;a;b)
⊢ ∃u:|g|. ((g-unit(u)) c∧ (a = (u * b) ∈ |g|))

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  Cancel(|g|;|g|;*)
3.  a  :  |g|
4.  b  :  |g|
5.  a  \msim{}  b
\mvdash{}  \mexists{}u:|g|.  ((g-unit(u))  c\mwedge{}  (a  =  (u  *  b)))


By

---

Latex:
Unfold  `cancel`  2  THEN  Unfold  `massoc`  5

---

Home Index