, Proceedings, vol.564, pp.163-179, 2013.

A. Grabowski, A. Korni?owicz, and C. Schwarzweller, On algebraic hierarchies 566 in mathematical repository of Mizar, 2016 Federated Conference on Computer Science and 567 Information Systems (FedCSIS), pp.363-371, 2016.

J. Hölzl, F. Immler, and B. Huffman, Type classes and filters for mathematical 569 analysis in Isabelle/HOL, Interactive Theorem Proving -4th International Conference, 570 ITP 2013, pp.279-294, 2013.

A. Mahboubi and E. Tassi, Canonical structures for the working coq user, p.573
URL : https://hal.archives-ouvertes.fr/hal-00816703

, Theorem Proving -4th International Conference, ITP 2013, 2013.

, Proceedings, pp.19-34, 2013.

, The Lean mathematical library, Proceedings of the 9th ACM 576 SIGPLAN International Conference on Certified Programs and Proofs, vol.2020, pp.367-381, 2020.

D. Miller and G. Nadathur, Programming with Higher-Order Logic, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00776197

F. Pfenning and C. Elliott, Higher-order abstract syntax, Proceedings of the 582

A. Sigplan, Conference on Programming Language Design and Implementation, p.583, 1988.

, PLDI '88, vol.584, pp.199-208, 1988.

R. Pollack, Dependently typed records in type theory, Formal Aspects of Computing, vol.586, pp.386-402, 2002.

F. Rabe and M. Kohlhase, A scalable module system. Information and Com-588 putation, vol.230, pp.1-54, 2013.

D. Rouhling, Formalisation Tools for Classical Analysis -A Case Study in Control Theory
URL : https://hal.archives-ouvertes.fr/tel-02333396

A. Saïbi, Typing algorithm in type theory with inheritance, 24th ACM SIGPLAN-593 SIGACT Symposium on Principles of Programming Languages, vol.594, pp.292-301, 1997.

A. Saïbi, Outils Génériques de Modélisation et de Démonstration pour la Formalisation 596

, des Mathématiques en Théorie des Types. Application à la Théorie des Catégories. (Formal-597 ization of Mathematics in Type Theory. Generic tools of Modelisation and Demonstration

, Application to Category Theory), vol.599, 1999.

K. Sakaguchi, Validating mathematical structures, accepted in the proceedings of 601 IJCAR 2020, 2020.

B. Spitters and E. Van-der-weegen, Type classes for mathematics in type theory

, Structures in Computer Science, vol.21, issue.4, pp.795-825, 2011.

E. Tassi and . Coq-elpi, Coq plugin embedding Elpi, vol.605

, Context (A : Type) (f : Ring_of_AbelianGroup A), HB.builders

, Fact mul0r : left_zero zero mul

, 65 move=> x; rewrite -[LHS]add0r addrC. 66 rewrite -{2}(addNr (mul x x)) (addrC (opp _)) addrA

, Fact mulr0 : right_zero zero mul