Proving correctness of an iterative Fibonacci algorithm

Question

One of the questions in the problem sets that I'm struggling in is this specific number that asks me to prove an iterative Fibonacci algorithm. The algorithm is written below:

function fib(n)
    if n = 0 then
        return(0)
    else
        a = 0; b = 1; i = 2;
        while i <= n do
            c = a + b
            a = b
            b = c
            i = i + 1
    return(b)

The way too prove correctness, according to my professor was to make sure that there are these three steps:

1. Initialization - the loop invariant must hold true prior to the first iteration
2. Maintenance - the loop invariant must hold true after an iteration
3. Termination - the loop invariant must hold true when the loop terminates

The loop invariant I've chosen is a <= b since I find this to be true for steps 1 through 3. First of all, I'm not sure if this is a valid loop invariant and this is the only observation I saw since i <= n isn't always true for inputs n that are natural numbers.

Assuming that I've chosen the correct loop invariant, I need to answer the proof by doing three steps so for this number I plan to answer it this way

1. Initialization - before the start of the loop a is assigned a value of 0 while b is assigned a value of 1 which starts the Fibonacci sequence. a <= b holds true prior to the start of the loop
2. Maintenance - during the loop, another variable c is added such that it is equal to the sum of a and b. After which, b is assigned to variable a while c is assigned to b thus making the invariant a <= b true during the iteration.
3. Termination - the loop ends when i > n. Before i is incremented, the procedures in the maintenance step is still done, thus the loop invariant still holds true

For my questions, is my loop invariant a <= b correct? And are the three statements I mentioned above sufficient to prove the correctness of an iterative Fibonacci algorithm?