---

Step * 1 2 1 of Lemma minus-poly-equiv


1. ∀i:ℕ||[]||. ∀j:ℕi.  imonomial-less([][j];[][i])
⊢ ipolynomial-term(minus-poly([])) ≡ "-"ipolynomial-term([])
BY
{ (Auto THEN RepUR ``minus-poly ipolynomial-term`` 0 THEN D 0 THEN Auto THEN RepUR ``int_term_value`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}i:\mBbbN{}||[]||.  \mforall{}j:\mBbbN{}i.    imonomial-less([][j];[][i])
\mvdash{}  ipolynomial-term(minus-poly([]))  \mequiv{}  "-"ipolynomial-term([])


By

---

Latex:
(Auto
  THEN  RepUR  ``minus-poly  ipolynomial-term``  0
  THEN  D  0
  THEN  Auto
  THEN  RepUR  ``int\_term\_value``  0
  THEN  Auto)

---

Home Index