theorem CD: :: NEWTON03:54

for b being non zero Nat
for a being non trivial Nat holds
( a divides b iff a |-count (a gcd b) = 1 )