Step
*
of Lemma
fib_coprime
∀n:ℕ. CoPrime(fib(n),fib(n + 1))
BY
{ ((D 0 THENM OnVar `n' NatInd) THENA Auto) }
1
.....basecase..... 
CoPrime(fib(0),fib(0 + 1))
2
.....upcase..... 
1. n : ℤ@i
2. [%1] : 0 < n@i
3. CoPrime(fib(n - 1),fib((n - 1) + 1))
⊢ CoPrime(fib(n),fib(n + 1))
Latex:
Latex:
\mforall{}n:\mBbbN{}.  CoPrime(fib(n),fib(n  +  1))
By
Latex:
((D  0  THENM  OnVar  `n'  NatInd)  THENA  Auto)
Home
Index