Coq is usually called an interactive theorem prover, not an automated prover. Interactive provers tend to accumulate varying degrees of automation.
Coq is a project at the scale of other niche programming languages. It is more of a platform than Z3 is. Z3 is more of a solver than a platform.
Coq has many, many moving parts. At it's core it has a dependently typed functional programming language and specification language called Gallina. But around that is built something called the tactic system, which slightly or signifcantly automates proof steps. On top of that there are scripting system like Ltac or plugins for specialized solvers. Coq also basically requires IDE support of sorts, as the proving process is a kind of REPL converation with the system.
Coq is vastly more expressive than Z3, so it makes sense that anything expressible in Z3 is expressible in Coq. What may be more surprising to people who have taken introductory tutorials is that there is significant automation in Coq, it just takes more effort and expertise than Z3's. In principle Coq could use Z3 as a plugin https://smtcoq.github.io/ but the other direction would make no sense at the moment. Z3 is the better choice for large scale but conceptually simple queries or proofs, such as a theorem just involving linear inequalities, arrays, Ands, and Ors, or for solving constraint problems. Coq is the better choice for almost anything more complex than that.
I do agree that they are usually not mentioned as competitors. Z3 does indeed basically find things, and Coq does mostly just verify things and not find them for you.
Coq is a project at the scale of other niche programming languages. It is more of a platform than Z3 is. Z3 is more of a solver than a platform.
Coq has many, many moving parts. At it's core it has a dependently typed functional programming language and specification language called Gallina. But around that is built something called the tactic system, which slightly or signifcantly automates proof steps. On top of that there are scripting system like Ltac or plugins for specialized solvers. Coq also basically requires IDE support of sorts, as the proving process is a kind of REPL converation with the system.
Coq is vastly more expressive than Z3, so it makes sense that anything expressible in Z3 is expressible in Coq. What may be more surprising to people who have taken introductory tutorials is that there is significant automation in Coq, it just takes more effort and expertise than Z3's. In principle Coq could use Z3 as a plugin https://smtcoq.github.io/ but the other direction would make no sense at the moment. Z3 is the better choice for large scale but conceptually simple queries or proofs, such as a theorem just involving linear inequalities, arrays, Ands, and Ors, or for solving constraint problems. Coq is the better choice for almost anything more complex than that.