/*
 * Definition of divisibility and greatest common divisor.
 *
 * Note: these definitions assume that their arguments are natural numbers.
 */
DEFINITIONS
    Divides (d, n) == (#kk . (kk : NATURAL & (n) = kk*(d)))
    ;
    /*
     * CD (p, x, y) means that p is a common divisor of x and y.
     */
    CD (p, x, y) == (Divides((p), (x)) & Divides((p), (y)))
    ;
    /*
     * GCD (p, x, y) means that p is the greatest common divisor of x and y.
     */
    GCD (p, x, y) ==
        (CD((p), (x), (y)) &
         !qq . (qq : NATURAL & CD(qq, (x), (y)) => qq <= (p)))
