---

Step * of Lemma l_sum_nonneg

∀[L:ℤ List]. ((∀x∈L.0 ≤ x) ⇒ (0 ≤ l_sum(L)))
BY
{ ((InstLemma `l_sum-lower-bound` [⌜0⌝]⋅ THENA Auto) THEN RepeatFor 2 (ParallelLast') THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L:\mBbbZ{}  List].  ((\mforall{}x\mmember{}L.0  \mleq{}  x)  {}\mRightarrow{}  (0  \mleq{}  l\_sum(L)))


By

---

Latex:
((InstLemma  `l\_sum-lower-bound`  [\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RepeatFor  2  (ParallelLast')  THEN  Auto)

---

Home Index