Ce projet développe une bibliothèque Rocq qui traduit automatiquement une partie de la bibliothèque HOL-Light, notamment la définition des nombres réels et des fonctions associées, vers des types et fonctions compatibles avec MathComp. L'objectif est de permettre l'utilisation de théorèmes HOL-Light dans des développements Rocq, facilitant ainsi l'interopérabilité entre ces environnements de preuve formelle. Les preuves traduites sont fournies comme axiomes pour une intégration rapide, tout en restant vérifiables via un script dédié.