---

Step * 1 of Lemma grp_lt_shift_right


1. g : OGrp
2. a : |g|
3. b : |g|
⊢ uiff(a < b;e < (b * (~ a)))
BY
{ ((InstLemma `grp_lt_op_l` [⌜g⌝;⌜a⌝;⌜b⌝;⌜~ a⌝]⋅ THENA Auto)
   THEN ParallelLast
   THEN (RW AbGrpNormC 0 THEN Auto)⋅
   THEN RW AbGrpNormC (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  OGrp
2.  a  :  |g|
3.  b  :  |g|
\mvdash{}  uiff(a  <  b;e  <  (b  *  (\msim{}  a)))


By

---

Latex:
((InstLemma  `grp\_lt\_op\_l`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}\msim{}  a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelLast
  THEN  (RW  AbGrpNormC  0  THEN  Auto)\mcdot{}
  THEN  RW  AbGrpNormC  (-1)
  THEN  Auto)

---

Home Index