---

Step * 1 1 of Lemma grp_op_preserves_le


1. ∀[g:OCMon]. ∀[z:|g|].  ∀x,y:|g|.  ((x ≤ y) ⇒ ((z * x) ≤ (z * y)))
⊢ ∀[g:OCMon]. ∀[x,y,z:|g|].  (x * y) ≤ (x * z) supposing y ≤ z
BY
{ (Auto THEN HypBackchain THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(Auto  THEN  HypBackchain  THEN  Auto)

---

Home Index