---

Step * 2 of Lemma polynom_wf

.....falsecase..... 
1. n : ℕ
2. ∀n:ℕn. ((polynom(n) ∈ Type) ∧ (polynom(n) ⊆r polyform(n)))
3. ¬(n = 0 ∈ ℤ)
⊢ ({p:polynom(n - 1) List| polyform-lead-nonzero(n;p)}  ∈ Type)
∧ ({p:polynom(n - 1) List| polyform-lead-nonzero(n;p)}  ⊆r (polyform(n - 1) List))
BY
{ ((InstHyp [⌜n - 1⌝] 2⋅ THENA Auto) THEN Unfold `polyform-lead-nonzero` 0 THEN Auto) }

---

Latex:

---

Latex:
.....falsecase..... 
1.  n  :  \mBbbN{}
2.  \mforall{}n:\mBbbN{}n.  ((polynom(n)  \mmember{}  Type)  \mwedge{}  (polynom(n)  \msubseteq{}r  polyform(n)))
3.  \mneg{}(n  =  0)
\mvdash{}  (\{p:polynom(n  -  1)  List|  polyform-lead-nonzero(n;p)\}    \mmember{}  Type)
\mwedge{}  (\{p:polynom(n  -  1)  List|  polyform-lead-nonzero(n;p)\}    \msubseteq{}r  (polyform(n  -  1)  List))


By

---

Latex:
((InstHyp  [\mkleeneopen{}n  -  1\mkleeneclose{}]  2\mcdot{}  THENA  Auto)  THEN  Unfold  `polyform-lead-nonzero`  0  THEN  Auto)

---

Home Index