---

Step * of Lemma decidable__grp_lt

∀g:OCMon. ∀a,b:|g|.  Dec(a < b)
BY
{ ProveSpecializedLemma `decidable__set_lt` 1 [parm{i};g↓oset] ((AbReduceC ANDTHENC FoldsC ``grp_lt``)) }

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}a,b:|g|.    Dec(a  <  b)


By

---

Latex:
ProveSpecializedLemma  `decidable\_\_set\_lt`  1  [parm\{i\};g\mdownarrow{}oset
]  ((AbReduceC  ANDTHENC  FoldsC  ``grp\_lt``))

---

Home Index