---

Step * of Lemma add-poly-lemma1

∀p,q:iMonomial() List. ∀m:iMonomial().
  ((∀i:ℕ||p||. ∀j:ℕi.  imonomial-less(p[j];p[i]))
  ⇒ (∀i:ℕ||q||. ∀j:ℕi.  imonomial-less(q[j];q[i]))
  ⇒ (0 < ||p|| ⇒ imonomial-less(m;p[0]))
  ⇒ (0 < ||q|| ⇒ imonomial-less(m;q[0]))
  ⇒ 0 < ||add-ipoly(p;q)||
  ⇒ imonomial-less(m;add-ipoly(p;q)[0]))
BY
{ InductionOnList }

1
∀q:iMonomial() List. ∀m:iMonomial().
  ((∀i:ℕ||[]||. ∀j:ℕi.  imonomial-less([][j];[][i]))
  ⇒ (∀i:ℕ||q||. ∀j:ℕi.  imonomial-less(q[j];q[i]))
  ⇒ (0 < ||[]|| ⇒ imonomial-less(m;[][0]))
  ⇒ (0 < ||q|| ⇒ imonomial-less(m;q[0]))
  ⇒ 0 < ||add-ipoly([];q)||
  ⇒ imonomial-less(m;add-ipoly([];q)[0]))

2
1. u : iMonomial()
2. v : iMonomial() List
3. ∀q:iMonomial() List. ∀m:iMonomial().
     ((∀i:ℕ||v||. ∀j:ℕi.  imonomial-less(v[j];v[i]))
     ⇒ (∀i:ℕ||q||. ∀j:ℕi.  imonomial-less(q[j];q[i]))
     ⇒ (0 < ||v|| ⇒ imonomial-less(m;v[0]))
     ⇒ (0 < ||q|| ⇒ imonomial-less(m;q[0]))
     ⇒ 0 < ||add-ipoly(v;q)||
     ⇒ imonomial-less(m;add-ipoly(v;q)[0]))
⊢ ∀q:iMonomial() List. ∀m:iMonomial().
    ((∀i:ℕ||[u / v]||. ∀j:ℕi.  imonomial-less([u / v][j];[u / v][i]))
    ⇒ (∀i:ℕ||q||. ∀j:ℕi.  imonomial-less(q[j];q[i]))
    ⇒ (0 < ||[u / v]|| ⇒ imonomial-less(m;[u / v][0]))
    ⇒ (0 < ||q|| ⇒ imonomial-less(m;q[0]))
    ⇒ 0 < ||add-ipoly([u / v];q)||
    ⇒ imonomial-less(m;add-ipoly([u / v];q)[0]))

---

Latex:

---

Latex:
\mforall{}p,q:iMonomial()  List.  \mforall{}m:iMonomial().
    ((\mforall{}i:\mBbbN{}||p||.  \mforall{}j:\mBbbN{}i.    imonomial-less(p[j];p[i]))
    {}\mRightarrow{}  (\mforall{}i:\mBbbN{}||q||.  \mforall{}j:\mBbbN{}i.    imonomial-less(q[j];q[i]))
    {}\mRightarrow{}  (0  <  ||p||  {}\mRightarrow{}  imonomial-less(m;p[0]))
    {}\mRightarrow{}  (0  <  ||q||  {}\mRightarrow{}  imonomial-less(m;q[0]))
    {}\mRightarrow{}  0  <  ||add-ipoly(p;q)||
    {}\mRightarrow{}  imonomial-less(m;add-ipoly(p;q)[0]))


By

---

Latex:
InductionOnList

---

Home Index