---

Step * of Lemma mproper_div_cond

∀g:IAbMonoid. (Cancel(|g|;|g|;*) ⇒ (∀a,b:|g|.  (((a * b) | a) ⇒ (g-unit(b)))))
BY
{ UnivCD THENA Auto }

1
1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. a : |g|
4. b : |g|
5. (a * b) | a
⊢ g-unit(b)

---

Latex:

---

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


By

---

Latex:
UnivCD  THENA  Auto

---

Home Index