---

Step * of Lemma imonomial-less-transitive

∀[m1,m2,m3:iMonomial()].  (imonomial-less(m1;m3)) supposing (imonomial-less(m2;m3) and imonomial-less(m1;m2))
BY
{ (Auto THEN D -2 THEN D -1 THEN D 0) }

1
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))

2
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)
⊢ ↑imonomial-le(m1;m3)

---

Latex:

---

Latex:
\mforall{}[m1,m2,m3:iMonomial()].
    (imonomial-less(m1;m3))  supposing  (imonomial-less(m2;m3)  and  imonomial-less(m1;m2))


By

---

Latex:
(Auto  THEN  D  -2  THEN  D  -1  THEN  D  0)

---

Home Index