Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Add some useful function to Q of zarith
divisible_down_to a m
return the greatest multiple of m
smaller or equal than a
divisible_down_to a m
return the smallest multiple of m
greater or equal than a