---

Step * 1 1 of Lemma from-upto-is-nil


1. n : ℤ@i
2. m : ℤ@i
3. [n, m) = [] ∈ (ℤ List)
⊢ m ≤ n
BY
{ Assert ⌜||[n, m)|| = 0 ∈ ℤ⌝⋅ }

1
.....assertion..... 
1. n : ℤ@i
2. m : ℤ@i
3. [n, m) = [] ∈ (ℤ List)
⊢ ||[n, m)|| = 0 ∈ ℤ

2
1. n : ℤ@i
2. m : ℤ@i
3. [n, m) = [] ∈ (ℤ List)
4. ||[n, m)|| = 0 ∈ ℤ
⊢ m ≤ n

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}@i
2.  m  :  \mBbbZ{}@i
3.  [n,  m)  =  []
\mvdash{}  m  \mleq{}  n


By

---

Latex:
Assert  \mkleeneopen{}||[n,  m)||  =  0\mkleeneclose{}\mcdot{}

---

Home Index