---

Step * of Lemma grp_op_preserves_le

∀[g:OCMon]. ∀[x,y,z:|g|].  (x * y) ≤ (x * z) supposing y ≤ z
BY
{ AssertLemma `ocmon_6` [] }

1
1. ∀[g:OCMon]. ∀[z:|g|].  monot(|g|;x,y.↑(x ≤b y);λw.(z * w))
⊢ ∀[g:OCMon]. ∀[x,y,z:|g|].  (x * y) ≤ (x * z) supposing y ≤ z

---

Latex:

---

Latex:
\mforall{}[g:OCMon].  \mforall{}[x,y,z:|g|].    (x  *  y)  \mleq{}  (x  *  z)  supposing  y  \mleq{}  z


By

---

Latex:
AssertLemma  `ocmon\_6`  []

---

Home Index