---

Step * of Lemma iseg_product-positive

∀[i,j:ℕ].  (0 < iseg_product(i;j)) supposing ((i ≤ j) and 0 < i)
BY
{ (Auto THEN Unfold `iseg_product` 0 THEN BLemma `combinations-positive` THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[i,j:\mBbbN{}].    (0  <  iseg\_product(i;j))  supposing  ((i  \mleq{}  j)  and  0  <  i)


By

---

Latex:
(Auto  THEN  Unfold  `iseg\_product`  0  THEN  BLemma  `combinations-positive`  THEN  Auto')

---

Home Index