---

Step * 1 1 1 of Lemma unique_mfact


1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. ∀a,b:|g|.  Dec(a | b)
4. g-unit(e)
⊢ [] ≡ [] upto ~
BY
{ TACTIC:((StrengthenRel) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  Cancel(|g|;|g|;*)
3.  \mforall{}a,b:|g|.    Dec(a  |  b)
4.  g-unit(e)
\mvdash{}  []  \mequiv{}  []  upto  \msim{}


By

---

Latex:
TACTIC:((StrengthenRel)  THEN  Auto)\mcdot{}

---

Home Index