---

Step * of Lemma nat_add_mon_wf

<ℕ,+> ∈ GrpSig
BY
{ Unfolds ``nat_add_mon grp_sig`` 0 THEN Auto' }

---

Latex:

---

Latex:
<\mBbbN{},+>  \mmember{}  GrpSig


By

---

Latex:
Unfolds  ``nat\_add\_mon  grp\_sig``  0  THEN  Auto'

---

Home Index