Ce projet propose une collection de modules et de fonctionnalités destinées à enrichir la bibliothèque standard de Rocq, un assistant de preuve formelle. Il vise à faciliter le développement de preuves mathématiques et logiques en fournissant des outils réutilisables et des abstractions supplémentaires.