---

Step * of Lemma minus-polynom_wf2

∀[n:ℕ]. ∀[p:polynom(n)].  (minus-polynom(n;p) ∈ polynom(n))
BY
{ (InductionOnNat
   THEN Intro
   THEN Unhide
   THEN (RecUnfold `polynom` (-1) THEN (OReduce (-1) THENA Auto))
   THEN DSetVars
   THEN RecUnfold `polynom` 0
   THEN RecUnfold `minus-polynom` 0
   THEN Reduce 0
   THEN (OReduce 0 THENA Auto)) }

1
1. n : ℤ
2. p : ℤ
⊢ -p ∈ ℤ

2
1. n : ℤ
2. 0 < n
3. ∀[p:polynom(n - 1)]. (minus-polynom(n - 1;p) ∈ polynom(n - 1))
4. p : polynom(n - 1) List
5. polyform-lead-nonzero(n;p)
⊢ if n=0 then -p else map-rev(λq.minus-polynom(n - 1;q);p) ∈ {p:polynom(n - 1) List| polyform-lead-nonzero(n;p)} 

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[p:polynom(n)].    (minus-polynom(n;p)  \mmember{}  polynom(n))


By

---

Latex:
(InductionOnNat
  THEN  Intro
  THEN  Unhide
  THEN  (RecUnfold  `polynom`  (-1)  THEN  (OReduce  (-1)  THENA  Auto))
  THEN  DSetVars
  THEN  RecUnfold  `polynom`  0
  THEN  RecUnfold  `minus-polynom`  0
  THEN  Reduce  0
  THEN  (OReduce  0  THENA  Auto))

---

Home Index