---

Step * of Lemma length-minus-polynom

∀[n:ℕ+]. ∀[p:polyform(n)].  (||minus-polynom(n;p)|| = ||p|| ∈ ℤ)
BY
{ (Auto THEN RecUnfold `polyform` (-1)⋅ THEN (SplitOnHypITE -1  THENA Auto)) }

1
.....truecase..... 
1. n : ℕ+
2. p : ℤ
3. n = 0 ∈ ℤ
⊢ ||minus-polynom(n;p)|| = ||p|| ∈ ℤ

2
.....falsecase..... 
1. n : ℕ+
2. p : polyform(n - 1) List
3. ¬(n = 0 ∈ ℤ)
⊢ ||minus-polynom(n;p)|| = ||p|| ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[p:polyform(n)].    (||minus-polynom(n;p)||  =  ||p||)


By

---

Latex:
(Auto  THEN  RecUnfold  `polyform`  (-1)\mcdot{}  THEN  (SplitOnHypITE  -1    THENA  Auto))

---

Home Index