Divisor of a ratio in lowest terms
Completion Axiom (completion-of-denominator):
(equal (denominator x) (if (rationalp x) (denominator x) 1))
Guard for (denominator x):
(rationalp x)
