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