---

Step * of Lemma length-lastn

∀[A:Type]. ∀[L:A List]. ∀[n:ℕ].  ||lastn(n;L)|| = n ∈ ℤ supposing n ≤ ||L||
BY
{ (Unfold `lastn` 0 THEN Auto) }

1
1. A : Type
2. L : A List
3. n : ℕ
4. n ≤ ||L||
⊢ ||nth_tl(||L|| - n;L)|| = n ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[L:A  List].  \mforall{}[n:\mBbbN{}].    ||lastn(n;L)||  =  n  supposing  n  \mleq{}  ||L||


By

---

Latex:
(Unfold  `lastn`  0  THEN  Auto)

---

Home Index