---

Step * of Lemma mul-list-positive

No Annotations
∀L:ℕ+ List. 0 < Π(L) 
BY
{ (InductionOnList THEN Reduce 0 THEN Auto) }

1
1. u : ℕ+
2. v : ℕ+ List
3. 0 < Π(v) 
⊢ 0 < Π([u / v]) 

---

Latex:

---

Latex:
No  Annotations
\mforall{}L:\mBbbN{}\msupplus{}  List.  0  <  \mPi{}(L) 


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto)

---

Home Index