Making proofs in a hierarchy of mathematical structures

International audienceThe FoC language is dedicated to the development of certified computer algebra libraries. These libraries are based on a hierarchy of implementations of mathematical structures. A FoC structure, called a species, contains the declarations of primitive operations and axioms, the definitions of derived operations, and theorems with their proofs. It is built through inheritance steps from previously existing structures, which includes in particular the redefinition of an operation. In this paper, we show that such a redefinition may have an huge impact on some of the proofs of the species, and may even invalidate some of them. We also describe what information the FoC system can give to the user about the proofs he is doing. As a conclusion, we propose a coding style to minimize the number of proofs that must be redone after a redefinition