---

Step * 1 of Lemma mdivides_weakening


1. g : IAbMonoid@i'
2. a : |g|@i
3. b : |g|@i
4. a ~ b@i
⊢ a | b
BY
{ D 4 THEN Trivial }

---

Latex:

---

Latex:

1.  g  :  IAbMonoid@i'
2.  a  :  |g|@i
3.  b  :  |g|@i
4.  a  \msim{}  b@i
\mvdash{}  a  |  b


By

---

Latex:
D  4  THEN  Trivial

---

Home Index