---

Step * 1 of Lemma grp_op_preserves_lt


1. g : OCMon
2. u : |g|
3. v : |g|
4. w : |g|
5. v < w
⊢ (u * v) < (u * w)
BY
{ ((OnMCls [0;5] (RWH (LemmaC `grp_lt_is_sp_of_leq_a`))) THEN Auto) }

1
1. g : OCMon
2. u : |g|
3. v : |g|
4. w : |g|
5. v ≤ w
6. ¬(w ≤ v)
⊢ (u * v) ≤ (u * w)

2
1. g : OCMon
2. u : |g|
3. v : |g|
4. w : |g|
5. v ≤ w
6. ¬(w ≤ v)
7. (u * v) ≤ (u * w)
⊢ ¬((u * w) ≤ (u * v))

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  u  :  |g|
3.  v  :  |g|
4.  w  :  |g|
5.  v  <  w
\mvdash{}  (u  *  v)  <  (u  *  w)


By

---

Latex:
((OnMCls  [0;5]  (RWH  (LemmaC  `grp\_lt\_is\_sp\_of\_leq\_a`)))  THEN  Auto)

---

Home Index