---

Step * 1 1 of Lemma increasing-sequence-prop1

.....upcase..... 
1. n : ℕ
2. a : ℕ ⟶ ℕ
3. increasing-sequence(a)
4. k : ℤ
5. 0 < k
6. (a n) ≤ (a (n + (k - 1)))
⊢ (a n) ≤ (a (n + k))
BY
{ (Unfold `increasing-sequence` (-4)
   THEN (InstHyp [⌜n + (k - 1)⌝] (-4)⋅ THENA Auto)
   THEN (Subst ⌜(n + (k - 1)) + 1 ~ n + k⌝ (-1)⋅ THENA Auto)) }

1
1. n : ℕ
2. a : ℕ ⟶ ℕ
3. ∀n:ℕ. (((a (n + 1)) = (a n) ∈ ℕ) ∨ ((a (n + 1)) = ((a n) + 1) ∈ ℕ))
4. k : ℤ
5. 0 < k
6. (a n) ≤ (a (n + (k - 1)))
7. ((a (n + k)) = (a (n + (k - 1))) ∈ ℕ) ∨ ((a (n + k)) = ((a (n + (k - 1))) + 1) ∈ ℕ)
⊢ (a n) ≤ (a (n + k))

---

Latex:

---

Latex:
.....upcase..... 
1.  n  :  \mBbbN{}
2.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
3.  increasing-sequence(a)
4.  k  :  \mBbbZ{}
5.  0  <  k
6.  (a  n)  \mleq{}  (a  (n  +  (k  -  1)))
\mvdash{}  (a  n)  \mleq{}  (a  (n  +  k))


By

---

Latex:
(Unfold  `increasing-sequence`  (-4)
  THEN  (InstHyp  [\mkleeneopen{}n  +  (k  -  1)\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}(n  +  (k  -  1))  +  1  \msim{}  n  +  k\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto))

---

Home Index