About Mathematical Components is the name of a library of formalized mathematics for the Coq proof assistants. It covers a variety of topics, from the theory of basic data structures (e.g., numbers, lists, finite sets) to more advanced results in various flavors of algebra. This library constitutes the infrastructure for the machine checked proofs of the Four Color Theorem and of the Odd Order The