---

Step * 1 1 1 of Lemma nth-fibs

.....subterm..... T:t
1:n
1. n : {1...}
2. n - 1 ≠ 0
3. ∀n:ℕn. (s-nth(n;fibs()) = fib(n) ∈ ℤ)
⊢ s-nth(n - 1 - 1;fibs()) = fib(n - 2) ∈ ℤ
BY
{ (RWO "-1" 0 THEN Auto)⋅ }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  n  :  \{1...\}
2.  n  -  1  \mneq{}  0
3.  \mforall{}n:\mBbbN{}n.  (s-nth(n;fibs())  =  fib(n))
\mvdash{}  s-nth(n  -  1  -  1;fibs())  =  fib(n  -  2)


By

---

Latex:
(RWO  "-1"  0  THEN  Auto)\mcdot{}

---

Home Index