---

Step * 2 1 1 of Lemma mul-ipoly_wf


1. u : iMonomial()
2. v : iMonomial() List
3. ∀i:ℕ||[u / v]||. ∀j:ℕi.  imonomial-less([u / v][j];[u / v][i])
4. q : iPolynomial()
5. i : ℕ||v||
6. j : ℕi
⊢ imonomial-less(v[j];v[i])
BY
{ ((InstHyp [⌜i + 1⌝;⌜j + 1⌝] 3⋅ THENA Auto) THEN NthHypEq (-1) THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  iMonomial()
2.  v  :  iMonomial()  List
3.  \mforall{}i:\mBbbN{}||[u  /  v]||.  \mforall{}j:\mBbbN{}i.    imonomial-less([u  /  v][j];[u  /  v][i])
4.  q  :  iPolynomial()
5.  i  :  \mBbbN{}||v||
6.  j  :  \mBbbN{}i
\mvdash{}  imonomial-less(v[j];v[i])


By

---

Latex:
((InstHyp  [\mkleeneopen{}i  +  1\mkleeneclose{};\mkleeneopen{}j  +  1\mkleeneclose{}]  3\mcdot{}  THENA  Auto)  THEN  NthHypEq  (-1)  THEN  EqCD  THEN  Auto)

---

Home Index