---

Step * 1 2 of Lemma add-nat-missing-prop


1. m : {m:ℤ| (-1) ≤ m} @i
2. s1 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} @i
3. x : ℕ@i
4. y : ℕ@i
5. x ≤ y
6. ¬(x ∈ s1 @ [m + 1, y))
7. m < y
⊢ (x = y ∈ ℕ) ∨ ((x ≤ m) ∧ (¬(x ∈ s1)))
BY
{ ((RW ListC (-2) THENA Auto)
   THEN (RWO "not_over_or" (-2) THEN Auto)
   THEN (RW ListC (-2) THENA Auto)
   THEN (RWO "not_over_and" (-2) THENA Auto)
   THEN D (-2)
   THEN Try (Complete ((OrRight THEN Auto)))
   THEN Try (Complete ((OrLeft THEN Auto)))) }

---

Latex:



1.  m  :  \{m:\mBbbZ{}|  (-1)  \mleq{}  m\}  @i
2.  s1  :  \{L:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;L)  \mwedge{}  (\mforall{}x\mmember{}L.x  <  m)\}  @i
3.  x  :  \mBbbN{}@i
4.  y  :  \mBbbN{}@i
5.  x  \mleq{}  y
6.  \mneg{}(x  \mmember{}  s1  @  [m  +  1,  y))
7.  m  <  y
\mvdash{}  (x  =  y)  \mvee{}  ((x  \mleq{}  m)  \mwedge{}  (\mneg{}(x  \mmember{}  s1)))


By

((RW  ListC  (-2)  THENA  Auto)
  THEN  (RWO  "not\_over\_or"  (-2)  THEN  Auto)
  THEN  (RW  ListC  (-2)  THENA  Auto)
  THEN  (RWO  "not\_over\_and"  (-2)  THENA  Auto)
  THEN  D  (-2)
  THEN  Try  (Complete  ((OrRight  THEN  Auto)))
  THEN  Try  (Complete  ((OrLeft  THEN  Auto))))

---

Home Index