• prospectus Un texte d'introduction pour expliquer le potentiel de Coq dans l'enseignement des mathématiques et les motivations.
• sin_properties.v Une preuve de propriété simple de la fonction sinus qui fait appel au théorème des accroissements finis.