package coq-rational

Definition of integers as the usual symetric completion of a semi-group and of rational numbers as the product of integers and strictly positive integers quotiented by the usual relation. This implementation assumes two sets of axioms allowing to define quotient types and subset types. These sets of axioms should be proved coherent by mixing up the deliverable model and the setoid model (both are presented in Martin Hofmann' thesis).