---

Step * of Lemma mdivides_preorder

∀g:IAbMonoid. Preorder(|g|;x,y.x | y)
BY
{ RepUnfolds ``preorder trans refl`` 0 
THEN GenUnivCD THENA Auto 
 }

1
1. g : IAbMonoid@i'
2. a : |g|@i
⊢ a | a

2
1. g : IAbMonoid@i'
2. a : |g|@i
3. b : |g|@i
4. c : |g|@i
5. a | b@i
6. b | c@i
⊢ a | c

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid.  Preorder(|g|;x,y.x  |  y)


By

---

Latex:
RepUnfolds  ``preorder  trans  refl``  0 
THEN  GenUnivCD  THENA  Auto 

---

Home Index