FDL > PVS > Number Theory > divisibility > divides : const-decl

divides(mm, i): bool = EXISTS (k:int) : i = (mm * k);