---

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


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

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}@i
2.  m  :  \mBbbZ{}@i
3.  [n,  m)  =  []
4.  if  n  <z  m  then  m  -  n  else  0  fi    =  0
\mvdash{}  m  \mleq{}  n


By

---

Latex:
TACTIC:(SplitOnHypITE  -1    THEN  Auto)

---

Home Index