---

Step * 2 of Lemma from-upto-member-nat


1. n : ℕ
2. m : ℕ
3. k : ℕ
4. (n ≤ k) ∧ k < m
⊢ (k ∈ [n, m))
BY
{ (With ⌜k - n⌝ (D 0)⋅ THEN Auto' THEN (RWW "select-from-upto length-from-upto" 0 THEN Auto')⋅) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  k  :  \mBbbN{}
4.  (n  \mleq{}  k)  \mwedge{}  k  <  m
\mvdash{}  (k  \mmember{}  [n,  m))


By

---

Latex:
(With  \mkleeneopen{}k  -  n\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto'  THEN  (RWW  "select-from-upto  length-from-upto"  0  THEN  Auto')\mcdot{})

---

Home Index