Cette bibliothèque fournit des fichiers vernaculaires contenant une formalisation de l'analyse réelle pour l'assistant de preuve Coq. Elle est une extension conservative de la bibliothèque standard Reals avec un accent sur l'utilisabilité.