I feel it is a math induction proof. I tried to draw a picture to try to help with the inductive step but was unsuccessful (I only got the base case). I am sure there is a technique to prove loops like this.
$\textbf{Question}:$ How do I prove the following proposition below?
Proposition: Let $n\in \mathbb{N}$. Then, $f(n)=n$ where $f(n)$ is given by the below diagram.
Proof: Base case: $n=1$. Then, $0<1$ is true which means $i\leftarrow 0+1=1$. Repeating the loop, we know $\underbrace{i}_{1}<1$ is false. Thus, $i$ must be $1$ when the loop is complete. Hence, $f(1)=1$ which proves the base case.
Best Answer
We claim that $i = n$ after execution of the while loop. To prove this claim we make the auxiliary claim that $i \leq n$ is a loop invariant. That is, that $i \leq n$ holds on entry to the loop, and that it is maintained by each iteration of the loop.
When the loop terminates, we know that the loop condition is no longer true, that is, that $i \geq n$. Since $i \leq n$ is still true, we obtain $i=n$. Now for the details. The proof is an induction on the number of iterations of the loop. Since this style of reasoning is common when proving properties of programs, the fact that we are dealing with induction is often given for granted. To bring the connection to the fore, let's define $P_k$ as "$i \leq n$ after $k$ iterations of the loop."
After the assignment $i \leftarrow 0$, $i \leq n$ holds because no natural number is less than $0$. That is, our invariant holds when $0$ iterations of the loop have been completed. This proves the base case of the induction; that is, it establishes $P_0$.
Suppose that after $k$ iterations the loop is still running (that is, $i < n$) and $P_k$ holds ($i \leq n$). In this simple case, $i < n$ implies $i \leq n$; hence we can focus on what we can infer about the state of the program after $k+1$ iterations from $i<n$ being true after $k$ iterations.
Let's denote by $i_{k+1}$ the value of $i$ at the end of iteration $k+1$ and by $i_k$ the value of $i$ after $k$ iterations. (That is, at the beginning of iteration $k+1$.) The effect of the assignment $i \leftarrow i+1$ is to establish $i_{k+1} = i_k + 1$. Now, from $i_k < n$ follows immediately that $i_{k+1} \leq n$. With this we have proved that $i \leq n$ is a loop invariant of the program, which holds after iteration $k+1$ if it holds after iteration $k$; in particular, it holds at the end of the the last iteration of the loop. As mentioned above, this implies both $i \leq n$ and $i \not< n$, or $i = n$. Another way to put it is that $P_k$ is inductive.
Looking at a simple case like this it is easy to overlook the fact that termination of a loop is not a given. In general, one has to prove that the loop terminates to be able to say that "when the loop terminates, the invariant still holds." This is usually done by identifying an integer-valued function of the program state that decreases at each iteration and is bounded from below. If such a ranking function exists, then the number of iterations is necessarily bounded. For our loop, $n-i$ will do.
Two aspects of the proof deserve attention. One is the claim of the effect of the assignment $i \leftarrow i+1$. When reasoning about programs one chooses axioms that describe the effect of program statements on the program's state so that they reflect what programs actually do. So, the effect of the assignment, as far as the proof is concerned, is simply the application of the axiom governing assignments. Here I have (somewhat informally) followed the popular axiomatization due to Tony Hoare.
The second aspect worthy of note is how one comes up with loop invariants and ranking functions. There is no algorithm that will compute either. In practice people (and programs that reason about other programs) use heuristics.