---

Step * of Lemma polyform-lead-nonzero_wf

∀[n:ℕ]. ∀[p:polyform(n)].  (polyform-lead-nonzero(n;p) ∈ ℙ)
BY
{ (Auto THEN RecUnfold `polyform` (-1) THEN Unfold `polyform-lead-nonzero` 0 THEN SplitOnHypITE -1  THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[p:polyform(n)].    (polyform-lead-nonzero(n;p)  \mmember{}  \mBbbP{})


By

---

Latex:
(Auto
  THEN  RecUnfold  `polyform`  (-1)
  THEN  Unfold  `polyform-lead-nonzero`  0
  THEN  SplitOnHypITE  -1 
  THEN  Auto)

---

Home Index