---

Step * 6 of Lemma int_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-equiv" 0 THENA Auto) THEN BLemma `itermMinus_functionality` 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-equiv"  0  THENA  Auto)  THEN  BLemma  `itermMinus\_functionality`  THEN  Auto)

---

Home Index