Front2026051 (#126)

* hb, mc-analysis and rocqy on the front page

Author: mkerjean

documentation.html

@@ -14,7 +14,7 @@
 - [[https://math-comp.github.io/mcb/][Mathematical Components]] by Assia Mahboubi and Enrico Tassi
 - [[https://www.morikita.co.jp/books/book/3287][Formal Proof using Coq/SSReflect/MathComp: Start Formalization of Mathematics with Free Software]] by Manabu Hagiwara and Reynald Affeldt (in Japanese, 日本語)
 - [[http://ilyasergey.net/pnp/][Programs and Proofs: Mechanizing Mathematics with Dependent Types]] by Ilya Sergey
-- [[https://staff.aist.go.jp/reynald.affeldt/documents/karate-rocq.pdf][Karate-Coq, An Introduction to MathComp-Analysis]] by Reynald Affeldt
+- [[https://staff.aist.go.jp/reynald.affeldt/documents/karate-rocq.pdf][Karate-Rocq, An Introduction to MathComp-Analysis]] by Reynald Affeldt
 * @@html: 📒@@ SSReflect reference manual
 - [[https://hal.inria.fr/inria-00258384/en][A Small Scale Reflection Extension for the Coq system]] by Georges Gonthier, Assia Mahboubi, and Enrico Tassi
   + the same [[https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html][htmlized as a part]] of Coq reference manual

documentation.org

@@ -16,16 +16,25 @@
 
 * About
 
+#+BEGIN_EXPORT html
+
+<div style="float: right; width: 240px; margin: 5px 10px">
+<img alt="rocqy" src="rocqy-mathcomp.png" style="width: 240px">
+</div>
+
+#+END_EXPORT
+
 Welcome to Mathematical Components' web-page! 
 
 Mathematical Components are libraries of formalized mathematics
 developed using the [[https://rocq-prover.org/][Rocq]] prover. This project finds its roots
 in the [[https://www2.tcs.ifi.lmu.de/~abel/lehre/WS07-08/CAFR/4colproof.pdf][formal proof of the Four Color Theorem]]. It has been used for
 large scale formalization projects, including a formal proof of the
-[[https://inria.hal.science/hal-00816699/document][Odd Order (Feit-Thompson) Theorem]].
+[[https://inria.hal.science/hal-00816699/document][Odd Order (Feit-Thompson) Theorem]], and extended to [[https://github.com/math-comp/analysis][mathematical analysis]]. 
 
-The libraries are written using the [[https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html][SSReflect proof language]], now part of
-the standard distribution of the Rocq prover.
+The libraries are written using the [[https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html][SSReflect proof language]], now part of the
+standard distribution of the Rocq prover. They are built thanks to
+[[https://github.com/math-comp/hierarchy-builder][Hierarchy-Builder]], a Rocq plugin.
 
 This is an open source project, licensed under the CeCILL-B free
 software license agreement.