To formally verify simple things where a simple SMT solver does the job, why do you need a 40-year old beast like Coq? Even the very title of the article doesn't make much sense: why would you _want_ to translate Z3 to Coq? Coq is useful, not just for formally verifying things that are far more complicated, but also for formalising (simple) pure mathematical constructs (ref: the HoTT effort). Coq was used to formally verify an entire C compiler (ref: CompCert), which was a landmark achievement.

If you're looking for a middle-ground between SMT automation and proving things that automation fails at, see efforts like F*. There are several proof assistants that use Z3 as a backend.

Coq is the oldest and most mature proof assistant. There are simpler alternatives like Agda, Isabelle, and Lean, each with their own downsides for the simplicity that they offer. For instance, cubical type theory has been formalised in Agda, but I'm currently working on a project to formalise semi-cubical sets in Coq, a project that has been running for a year, and might not be completed.

Coq has a very advanced dependently-typed system, but as a result, the Coq unifier is heuristic-based, and fails at certain points without good diagnostics. That's where the Coq tactic system Ltac2 steps in: there is no other proof assistant that has such such an advanced tactic language.

TL;DR: Coq is a 40-year old ageing beast, and there is nothing quite as powerful. However, even it is immature when it comes to formalising higher categories or other similar graduate-level mathematics. It's painful to work with, because of the number of warts it has accumulated, but there is simply no alternative.