 Solution

Take the four-divergence of the Proca equation. Commuting partial derivatives and using that $F^{ab}$ is an antisymmetric second-rank tensor giveConsequently, for $m\ne 0$, ${\partial }_a{A}^a=0$. This is the Lorenz constraint in Proca theory: an equation of motion enforces it, rather than a choice of gauge fixing. It leaves $(\square -m^2)A^a=0$. At $m=0$ the divergence argument supplies no such constraint; the massless gauge symmetry requires a separate treatment.