In this work, we aim at the verification in Coq/Rocq of Beeson's main result in A constructive version of Tarski's geometry, namely that the arithmetization of geometry can be obtain without assuming any decidability property. Our first goal is to deal with the lemmas that do not assert the existence of some geometrical objects. This is what Beeson calls the "wholesale importation of proofs of negative theorems from classical to constructive geometry". Instead of relying on the Gödel double-negation interpretation, we work at the level of tactics, the language that allows to build proofs interactively. Reasoning steps that are not intuitionistically acceptable can still be performed under the assumption that they are used to prove a negative theorem, thus constructivizing the proofs. Thus, we rely on coq-ditto to automate the constructivization process. We report on the current progress towards this goal.