theorem :: NEWTON02:125

for a, b being Nat st b > 0 & a,b ! are_coprime holds
a,b are_coprime