Proof by induction Fibonacci Prove correctness of the following algorithm for computing the nth Fibonacci number.
algorithm fastfib (integer n) 
if n<0return0;
else if n = 0 return 0;
else if n = 1 return 1;
else a ← 1; b ← 0;
    for i from 2 to n do
       t ← a; a ← a + b; b ← t; 
return a;
end

Not 100% how to complete this with proof by induction. How I started:
Base case: The proof is by induction on n. consider the cases n = 0 and n = 1. in these cases,  the algorithm presented returns 0 and 1, which may as well be the 0th and 1st Fibonacci numbers. 
Now we assume that the algorithm return the correct Fibonacci number for n ( the nth Fibonacci number) for all n<= k where k >= 1. I wasn't sure if I was on right track and where to move from here. 
 A: You don't want to do induction on the fastfib routine as a whole, since it is not written as a recursive procedure (which is why it is fast, since the typical recursive routine is not) 
Instead, you want to do induction on the $i$ of the for loop. In particular, show that after you have done the operations inside the for loop for some value of $i$, $a$ equals Fibonacci number $i$, and $b$ equals Fibonacci number $i-1$
So, as the base you can take $i=2$: given that $a$ is initially set to 1, and $b$ to 0, after the operations $t \leftarrow a$ (so $t$ is set to 1), $a \leftarrow a +b$ (so now $a$ is 1), and $b \leftarrow t$ (so now $b$ is 1), we have indeed that $a=1=F_2$, and $b=1=F_1$. Check!
As a step: assume that after you have done the operations inside the for loop for $i=k$, we have that $a=F_k$ and $b=F_{k-1}$. So now when $i$ becomes $k+1$ and we do one more pass through the operations, we get:
$t \leftarrow a$: so $t=F_k$
$a \leftarrow a +b$: so $a=F_k+F_{k-1}=F_{k+1}$
$b \leftarrow t$: so $b=F_k$
So, $a=F_{k+1}$ and $b=F_k$, as desired. Check!
A: algorithm fastfib (integer n) 
    if      n < 0 return 0;
    else if n = 0 return 0;
    else if n = 1 return 1;
    else {
        a ← 1;
        b ← 0;
        for i from 2 to n do {
           #assert a = F(i - 1)
           #assert b = F(i - 2)
           t ← a;
           a ← a + b;
           b ← t; 
           #assert a = F(i)
           #assert b = F(i - 1)
        }
        #assert i = n + 1
        #assert a = F(i - 1)
        return a;
   }
end

Now you can prove the assertions with induction.
