theorem :: NEWTON03:64

for a, b being non zero Nat holds
( a gcd b = 1 iff for c being non trivial Nat holds (c |-count a) * (c |-count b) = 0 )