---

Step * of Lemma assert-nonneg-poly

∀[p:iPolynomial()]. uiff(↑nonneg-poly(p);(∀m∈p.↑nonneg-monomial(m)))
BY
{ ((D 0 THENA Auto) THEN Unfold `nonneg-poly` 0 THEN RWO  "assert-bl-all" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p:iPolynomial()].  uiff(\muparrow{}nonneg-poly(p);(\mforall{}m\mmember{}p.\muparrow{}nonneg-monomial(m)))


By

---

Latex:
((D  0  THENA  Auto)  THEN  Unfold  `nonneg-poly`  0  THEN  RWO    "assert-bl-all"  0  THEN  Auto)

---

Home Index