M. Aschbacher, Finite Group Theory. Cambridge Studies in Advanced Mathematics, 2000.

H. Bender and G. Glauberman, Local analysis for the Odd Order Theorem, NumberLNS, vol.188, 1994.
DOI : 10.1017/CBO9780511665592

Y. Bertot and P. Castéran, Interactive theorem proving and program development: Coq'Art: The calculus of inductive constructions, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

Y. Bertot, G. Gonthier, S. O. Biha, and I. Pasca, Canonical Big Operators, TPHOLs, pp.86-101, 2008.
DOI : 10.1007/3-540-44659-1_29
URL : https://hal.archives-ouvertes.fr/inria-00331193

N. G. De-bruijn, The mathematical language AUTOMATH, its usage, and some of its extensions, Symposium on Automatic Demonstration, pp.29-61, 1970.
DOI : 10.1007/BFb0060623

W. Feit and J. G. Thompson, Chapter I, from Solvability of groups of odd order, Pacific J. Math, vol. 13, no. 3 (1963, Pacific Journal of Mathematics, vol.13, issue.3, pp.775-1029, 1963.
DOI : 10.2140/pjm.1963.13.775

F. Garillot, Generic Proof Tools and Finite Group Theory, 2011.
URL : https://hal.archives-ouvertes.fr/pastel-00649586

G. Gonthier, Point-Free, Set-Free Concrete Linear Algebra, ITP, pp.103-118, 2011.
DOI : 10.1017/S0956796802004501
URL : https://hal.archives-ouvertes.fr/hal-00805966

G. Gonthier and A. Mahboubi, An introduction to small scale reflection in Coq, Journal of Formalized Reasoning, vol.3, issue.2, pp.95-152, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00515548

G. Gonthier, A. Mahboubi, L. Rideau, E. Tassi, and L. Théry, A Modular Formalisation of Finite Group Theory, TPHOLs, pp.86-101, 2007.
DOI : 10.1007/978-3-540-74591-4_8
URL : https://hal.archives-ouvertes.fr/inria-00139131

G. Gonthier, A. Mahboubi, and E. Tassi, A Small Scale Reflection Extension for the Coq system
URL : https://hal.archives-ouvertes.fr/inria-00258384

M. Hedberg, A coherence theorem for Martin-L??f's type theory, Journal of Functional Programming, vol.8, issue.4, pp.413-436, 1998.
DOI : 10.1017/S0956796898003153

O. Hölder, Zur???ckf???hrung einer beliebigen algebraischen Gleichung auf eine Kette von Gleichungen, Mathematische Annalen, vol.34, issue.1, pp.26-56, 1889.
DOI : 10.1007/BF01446791

I. Isaacs, Character Theory of Finite Groups, AMS Chelsea Pub. Series, 1976.
DOI : 10.1090/chel/359

C. Jordan, Traité des substitutions et deséquationsdeséquations algébriques, p.1870

H. Kurzweil and B. Stellmacher, The Theory of Finite Groups: An Introduction, 2010.
DOI : 10.1007/b97433

A. Mahboubi and E. Tassi, Canonical Structures for the Working Coq User, ITP 2013, 4th Conference on Interactive Theorem Proving, 2013.
DOI : 10.1007/978-3-642-39634-2_5
URL : https://hal.archives-ouvertes.fr/hal-00816703

T. Peterfalvi, Character Theory for the Odd Order Theorem, Number LNS, vol.272, 2000.
DOI : 10.1017/CBO9780511565861

F. Wiedijk, The " de Bruijn factor

H. Zassenhaus, Zum satz von Jordan-Hölder-Schreier, pp.106-108, 1934.