---

Step * 1 of Lemma mdivides_refl


1. g : IAbMonoid
2. a : |g|
⊢ a | a
BY
{ With e (D 0) THENA Auto }

1
1. g : IAbMonoid
2. a : |g|
⊢ a = (a * e) ∈ |g|

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  a  :  |g|
\mvdash{}  a  |  a


By

---

Latex:
With  e  (D  0)  THENA  Auto

---

Home Index