---

Step * 1 1 of Lemma not-imonomial-le


1. a1 : ℤ-o
2. a2 : {vs:ℤ List| sorted(vs)} 
3. b1 : ℤ-o
4. b2 : {vs:ℤ List| sorted(vs)} 
5. b2 = a2 ∈ (ℤ List)
⊢ ↑a2 ≤_lex a2
BY
{ (RWO "eqtt_to_assert<" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a1  :  \mBbbZ{}\msupminus{}\msupzero{}
2.  a2  :  \{vs:\mBbbZ{}  List|  sorted(vs)\} 
3.  b1  :  \mBbbZ{}\msupminus{}\msupzero{}
4.  b2  :  \{vs:\mBbbZ{}  List|  sorted(vs)\} 
5.  b2  =  a2
\mvdash{}  \muparrow{}a2  \mleq{}\_lex  a2


By

---

Latex:
(RWO  "eqtt\_to\_assert<"  0  THEN  Auto)

---

Home Index