# Using Hoare logic to show an invariant holds or using induction?

I want to know if given a while loop:

x = 0
while(x < 5){
x = x + 1
}


I want to show that x (at the a ith iteration of the loop), the value of i is assigned to x and x is never assigned the same value twice. Like we know that running code that the sequence of assignments is 0, 1, 2, 3, 4, 5. But in a theoretic sense a sequence of assignments like 0, 1, 1, 5 will still terminate the loop.

It's easy to do this via induction but I am having difficulty doing this with Hoare logic.

I want to know, if I show the loop invariant holds via induction can I then use the loop invariant in proving the algorithm with the while rule i.e. in the Hoare triple.