When Beeson started his project of computer-checking Euclid's Elements he used a set of $36$ axioms. They can we split into two kinds. 20 of them are Tarski-style axioms and the remaining $16$ are about the notion of equal figures. Then, at the Logic Colloquium 2019, he presented his approach of defining the concept of equal figures and how to prove that it verifies the axioms needed for computer-checking Euclid's Elements. This work was completed with "On the Notion of Equal Figures in Euclid". Our work aims at the formal verification in the Coq/Rocq proof assistant of the proofs from "On the Notion of Equal Figures in Euclid". This would not only guarantee that there is no hole in the proofs, but it would also allow to establish the mutual interpretability between the axioms used in "Proof-Checking Euclid" and the one used by Tarski and his co-authors in "Metamathematische Methoden in der Geometrie". We use the GeoCoq library as a basis for this work. Up to our knowledge, there is no formal verification of the results from "On the Notion of Equal Figures in Euclid".