Will that make it easier to write good code elsewhere? Almost certainly if you're not familiar with mathematical proof (maybe you took a discrete math course before). If you know what it is to prove then you'll learn an interesting deep connection between programming and proving.

You probably don't want to prove things in your programs. Not really. Even after you learn Coq it's too difficult to do day-to-day.

But proofs do not work without being completely consistent in the same way that good programs are. So you can learn a lot of techniques for good programs from techniques for good proofs. Coq rejects bad proofs, so it can be good practice.

Finally, Coq is unashamedly higher-order. The chops you gain working with it will translate more or less directly to better functional programming comprehension.

I was able to access highly technical programming jobs, those where you are using formal or semi-formal methods to build critical and/or real-time systems. These are very well paid and very nice to work on. You end up designing and implementing very elegant systems with nice guarantees. It feels like high-end engineering. So from a pragmatic point of view, you can access better jobs.

From a more idealistic perspective, you will understand computation better.