---

Step * 1 of Lemma imonomial-less-transitive


1. m1 : iMonomial()
2. m2 : iMonomial()
3. m3 : iMonomial()
4. ¬((snd(m1)) = (snd(m2)) ∈ (ℤ List))
5. ↑imonomial-le(m1;m2)
6. ¬((snd(m2)) = (snd(m3)) ∈ (ℤ List))
7. ↑imonomial-le(m2;m3)
⊢ ¬((snd(m1)) = (snd(m3)) ∈ (ℤ List))
BY
{ ((All (RWO "eqtt_to_assert<") THENA Auto)
   THEN DVar `m1'
   THEN DVar `m2'
   THEN DVar `m3'
   THEN All (RepUR ``imonomial-le``)⋅) }

1
1. m4 : ℤ-o
2. m5 : {vs:ℤ List| sorted(vs)} 
3. m6 : ℤ-o
4. m7 : {vs:ℤ List| sorted(vs)} 
5. m8 : ℤ-o
6. m9 : {vs:ℤ List| sorted(vs)} 
7. ¬((snd(<m4, m5>)) = (snd(<m6, m7>)) ∈ (ℤ List))
8. m5 ≤_lex m7 = tt
9. ¬((snd(<m6, m7>)) = (snd(<m8, m9>)) ∈ (ℤ List))
10. m7 ≤_lex m9 = tt
⊢ ¬((snd(<m4, m5>)) = (snd(<m8, m9>)) ∈ (ℤ List))

---

Latex:

---

Latex:

1.  m1  :  iMonomial()
2.  m2  :  iMonomial()
3.  m3  :  iMonomial()
4.  \mneg{}((snd(m1))  =  (snd(m2)))
5.  \muparrow{}imonomial-le(m1;m2)
6.  \mneg{}((snd(m2))  =  (snd(m3)))
7.  \muparrow{}imonomial-le(m2;m3)
\mvdash{}  \mneg{}((snd(m1))  =  (snd(m3)))


By

---

Latex:
((All  (RWO  "eqtt\_to\_assert<")  THENA  Auto)
  THEN  DVar  `m1'
  THEN  DVar  `m2'
  THEN  DVar  `m3'
  THEN  All  (RepUR  ``imonomial-le``)\mcdot{})

---

Home Index