In this paper we present a procedure used to translate the GeoCoq library, a Rocq formalization of proofs in geometry, into a First-Order Logic encoding in the logical framework \Dedukti. We describe the modifications made to the tool to permit this translation and the process that lead to the first-order simplification. As a result, this translation enables us to share the proofs to other proofs assistants.