---

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


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

---

Latex:

---

Latex:

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


By

---

Latex:
(RepUR  ``minus-poly  ipolynomial-term``  0  THEN  D  0  THEN  Reduce  0  THEN  Auto)

---

Home Index