---

Step * of Lemma l_sum-lower-bound

∀b:ℤ. ∀[L:ℤ List]. ((∀x∈L.b ≤ x) ⇒ ((b * ||L||) ≤ l_sum(L)))
BY
{ (InductionOnList
   THEN Unfold `l_sum` 0
   THEN Reduce 0
   THEN Try (Fold `l_sum` 0)
   THEN Try ((RWO "l_all_cons" 0 THEN Auto THEN ThinTrivial))
   THEN Auto') }

---

Latex:

---

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


By

---

Latex:
(InductionOnList
  THEN  Unfold  `l\_sum`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `l\_sum`  0)
  THEN  Try  ((RWO  "l\_all\_cons"  0  THEN  Auto  THEN  ThinTrivial))
  THEN  Auto')

---

Home Index