---

Step * of Lemma assert_of_grp_blt

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

---

Latex:

---

Latex:
\mforall{}[g:OCMon].  \mforall{}[a,b:|g|].    uiff(\muparrow{}(a  <\msubb{}  b);a  <  b)


By

---

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

---

Home Index