---

Step * of Lemma last-from-upto

∀[n,m:ℤ].  last([n, m)) ~ m - 1 supposing n < m
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `last` 0
   THEN (RWO "length-from-upto" 0 THENA Auto)
   THEN AutoSplit
   THEN (RWO "select-from-upto" 0 THENA Auto)
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbZ{}].    last([n,  m))  \msim{}  m  -  1  supposing  n  <  m


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `last`  0
  THEN  (RWO  "length-from-upto"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  (RWO  "select-from-upto"  0  THENA  Auto)
  THEN  Auto')

---

Home Index