x = n
while x > 0:
x = x // 2
Let $x_k$ denote the variable x after $k$ iterations.
How do I prove by induction that $\forall n \in \mathbb{Z}^+, \forall k \in \mathbb{N}, \frac{n}{2^k} - \frac{2^k - 1}{2^k} \leq x_k \leq \frac{n}{2^k} $?
Given: $\forall x\in \mathbb{Z}, \frac{x -1}{2} \leq \lfloor \frac{x}{2} \rfloor \leq \frac{x}{2}$.
I started off by thinking what $x_k$ should be. I think it is something like $\lfloor n / 2\rfloor^k$ but I have a feeling this is wrong? Could anyone guide me in the right direction and provide a clue to the induction?
$x_k$ is what you get when you write $n$ in base $2$ and erase the last $k$ bits (=binary digits). Specifically, the map $f : x \mapsto \lfloor x/2 \rfloor$ erases one bit from $x$. For example, if $n = 110110101011_2$ then $x_4 = 11011010_2$.
If the last $k$ bits are $0$ then $x_k$ is exactly $n/2^k$. If the last $k$ bits are $1$, then because $11\dots11_2 = 1 + 2 + \dots + 2^{k-1} = 2^k - 1$, $$ x_k = \frac{n - (2^k - 1)}{2^k} $$ since subtracting $2^k - 1$ zeroes the last $k$ bits. In general, it follows that $x_k$ must be between these two extremes.
Now, if you want to prove this inductively, you need an inductive definition. That being $x_k = f(x_{k-1})$. So $x_0 = n$ and $x_1 = \lfloor n/2 \rfloor$ and $x_2 = \lfloor \lfloor n/2 \rfloor /2 \rfloor$ and $x_3 = \lfloor \lfloor \lfloor n/2 \rfloor /2 \rfloor/2 \rfloor$ and so forth.
So now you assume that $$\frac n{2^k} - \frac{2^k - 1}{2^k} \le x_k \le \frac n{2^k} \tag{1}$$ (the inductive hypothesis). Then use the inequality you mentioned with $f(x)$ to obtain
$$ \frac{x_k -1}{2} \leq x_{k+1}= \left\lfloor \frac{x_k}{2} \right\rfloor \leq \frac{x_k}{2}. \tag{2}$$
Combine $(1)$ and $(2)$ and you have what you want.