Coq.Interval - Bibliothèque Coq.Interval de preuve automatique de bornes sur des expressions à valeurs réelles Date de dernière version : 15 septembre 2017
La bibliothèque Coq.Interval fournit des tactiques pour l'asistant de preuves Coq servant à faciliter la preuve d'inéqualités sur des expressions à valeurs réelles.