---

Step * 6 of Lemma real_term_polynomial


1. num : int_term()
2. ipolynomial-term(int_term_to_ipoly(num)) ≡ num
⊢ ipolynomial-term(minus-poly(int_term_to_ipoly(num))) ≡ "-"num
BY
{ ((RWO "minus-poly-req" 0 THENA Auto) THEN RWO "-1" 0 THEN Auto THEN RelRST THEN Auto) }

---

Latex:

---

Latex:

1.  num  :  int\_term()
2.  ipolynomial-term(int\_term\_to\_ipoly(num))  \mequiv{}  num
\mvdash{}  ipolynomial-term(minus-poly(int\_term\_to\_ipoly(num)))  \mequiv{}  "-"num


By

---

Latex:
((RWO  "minus-poly-req"  0  THENA  Auto)  THEN  RWO  "-1"  0  THEN  Auto  THEN  RelRST  THEN  Auto)

---

Home Index