Proof verification: powers of a group element of finite order are distinct

Almost.

You assert $b-a < n$. I think you want to assume $b \ge a$ (without loss of generality) from the start, to make $b-a$ nonnegative as well. Otherwise you need to handle the case when it's not.

Logically, everything looks good, except for @Ethan's point. If you are worried about circularity, make sure you understand why your statement “$x^{b-a} = 1 \implies b-a =0$” is true.

I think notations like

Let $a,b\in[0,n-1] \cap \mathbb{N}$ such that $x^a = x^b$.

are a bit cumbersome. Personally, I would rewrite the first sentence as

Let $a$ and $b$ be integers such that $0 \leq a \leq b \leq n-1$ and $x^a = a^b$.

Or perhaps even

Suppose $x^a = x^b$ for some integers $a$ and $b$ with $0 \leq a\leq b\leq n-1$.

In essence, you want to show $x^a = x^b \implies a=b$, so writing the first sentence that way aligns the paragraph with that logical statement.

Having a higher density of symbols does not make a more mathematically sophisticated argument.

Your proof is perfectly fine. Good Job!

One remark: One prof of me uses the following convention: $[0:n] := [0, n] \cap \mathbb N$.

This is an elegant way to write such "discrete intervals" and makes proofs more readable. Just an idea of me. Maybe you want to use it :)