---

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

.....assertion..... 
∀n,m:ℤ.  ([n, m) = [] ∈ (ℤ List) ⇐⇒ m ≤ n)
BY
{ TACTIC:Auto }

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

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

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}n,m:\mBbbZ{}.    ([n,  m)  =  []  \mLeftarrow{}{}\mRightarrow{}  m  \mleq{}  n)


By

---

Latex:
TACTIC:Auto

---

Home Index