I didn't mean this by "reasoning". To me, Coq does not reason (in the meaning I intended). It checks proofs are well-formed and assists proof writing.
But yes, there's some implementation of logic in Coq. It applies (a specific form of) logic. Again, LLMs output probable text. They don't do logic. They do statistics on language.
Coq works on the actual objects themselves directly, not on the text that presents them.
LLMs usually fail to answer to riddles correctly for this reason. We saw plenty of occurrences of this in recent times. Each time LLMs are benchmarked, people think of trying riddles and it works to some extent because something that looks like these riddles are in the training set but it eventually fails. Humans also make mistakes when solving riddles, but not for the same reasons (the process is not the same, they are not "processing text", the are really processing logic, even if the process is fallible).