---

Step * of Lemma mdivides_cancel

∀g:IAbMonoid. (Cancel(|g|;|g|;*) ⇒ (∀a,b,c:|g|.  (((a * b) | (a * c)) ⇒ (b | c))))
BY
{ ((UnivCD) THEN Auto) 
THEN (UnfoldTopAb 2) }

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. c : |g|
6. (a * b) | (a * c)
⊢ b | c

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid.  (Cancel(|g|;|g|;*)  {}\mRightarrow{}  (\mforall{}a,b,c:|g|.    (((a  *  b)  |  (a  *  c))  {}\mRightarrow{}  (b  |  c))))


By

---

Latex:
((UnivCD)  THEN  Auto) 
THEN  (UnfoldTopAb  2)

---

Home Index