---

Step * 1 2 1 of Lemma polynom-equal-iff


1. n : ℤ
2. p : polynom(0)
3. q : polynom(0)
4. ↑poly-zero(0;add-polynom(0;tt;p;minus-polynom(0;q)))
⊢ p = q ∈ polynom(0)
BY
{ ((RecUnfold `polynom` 0 THEN Reduce 0)
   THEN (RecUnfold `polynom` 2 THEN Reduce 2)
   THEN (RecUnfold `polynom` 3 THEN Reduce 3)
   THEN (RecUnfold `minus-polynom` (-1) THEN RecUnfold `add-polynom` (-1))
   THEN RepUR ``poly-zero`` -1) }

1
1. n : ℤ
2. p : ℤ
3. q : ℤ
4. ↑(p + (-q) =z 0)
⊢ p = q ∈ ℤ

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  p  :  polynom(0)
3.  q  :  polynom(0)
4.  \muparrow{}poly-zero(0;add-polynom(0;tt;p;minus-polynom(0;q)))
\mvdash{}  p  =  q


By

---

Latex:
((RecUnfold  `polynom`  0  THEN  Reduce  0)
  THEN  (RecUnfold  `polynom`  2  THEN  Reduce  2)
  THEN  (RecUnfold  `polynom`  3  THEN  Reduce  3)
  THEN  (RecUnfold  `minus-polynom`  (-1)  THEN  RecUnfold  `add-polynom`  (-1))
  THEN  RepUR  ``poly-zero``  -1)

---

Home Index