---

Step * 1 1 of Lemma select-from-upto


1. d : ℤ
2. n : ℤ
3. m : ℤ
4. (m - n) ≤ 0
5. k : ℕm - n
⊢ [n, m)[k] ~ n + k
BY
{ TACTIC:Auto' }

---

Latex:

---

Latex:

1.  d  :  \mBbbZ{}
2.  n  :  \mBbbZ{}
3.  m  :  \mBbbZ{}
4.  (m  -  n)  \mleq{}  0
5.  k  :  \mBbbN{}m  -  n
\mvdash{}  [n,  m)[k]  \msim{}  n  +  k


By

---

Latex:
TACTIC:Auto'

---

Home Index