---

Step * 1 of Lemma equipollent-int_seg


1. n : ℤ
2. m : ℤ
3. ¬n < m
⊢ {n..m-} ~ ℕ0
BY
{ (With ⌜λx.(x - n)⌝ (D 0)⋅ THEN Auto THEN Auto' THEN RepeatFor 2 (D 0) THEN Reduce 0 THEN Auto THEN Auto') }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  \mneg{}n  <  m
\mvdash{}  \{n..m\msupminus{}\}  \msim{}  \mBbbN{}0


By

---

Latex:
(With  \mkleeneopen{}\mlambda{}x.(x  -  n)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  Auto'
  THEN  RepeatFor  2  (D  0)
  THEN  Reduce  0
  THEN  Auto
  THEN  Auto')

---

Home Index