---

Step * of Lemma before-upto

∀n:ℕ. ∀x,y:ℕn.  (x before y ∈ upto(n) ⇐⇒ x < y)
BY
{ (Unfold `l_before` 0 THEN Unfold `sublist` 0 THEN Reduce 0 THEN Auto THEN Reduce 0 THEN Auto' THEN ExRepD) }

1
1. n : ℕ
2. x : ℕn
3. y : ℕn
4. f : ℕ2 ⟶ ℕ||upto(n)||
5. increasing(f;2)
6. ∀j:ℕ2. ([x; y][j] = upto(n)[f j] ∈ ℕn)
⊢ x < y

2
1. n : ℕ
2. x : ℕn
3. y : ℕn
4. f : ℕ2 ⟶ ℕ||upto(n)||
5. increasing(f;2)
6. j : ℕ2
⊢ f j < n

3
1. n : ℕ
2. x : ℕn
3. y : ℕn
4. x < y
⊢ ∃f:ℕ2 ⟶ ℕ||upto(n)||. (increasing(f;2) ∧ (∀j:ℕ2. ([x; y][j] = upto(n)[f j] ∈ ℕn)))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}x,y:\mBbbN{}n.    (x  before  y  \mmember{}  upto(n)  \mLeftarrow{}{}\mRightarrow{}  x  <  y)


By

---

Latex:
(Unfold  `l\_before`  0
  THEN  Unfold  `sublist`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  Reduce  0
  THEN  Auto'
  THEN  ExRepD)

---

Home Index