---

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


1. n : ℤ@i
2. m : ℤ@i
3. [n, m) = [] ∈ (ℤ List)
4. ||[n, m)|| = 0 ∈ ℤ
⊢ m ≤ n
BY
{ TACTIC:((RWO "length-from-upto" (-1)) THEN Auto) }

1
1. n : ℤ@i
2. m : ℤ@i
3. [n, m) = [] ∈ (ℤ List)
4. if n <z m then m - n else 0 fi  = 0 ∈ ℤ
⊢ m ≤ n

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:((RWO  "length-from-upto"  (-1))  THEN  Auto)

---

Home Index