for a, b being non zero Nat st not a,b are_coprime holds
ex k being non zero Nat st
( k <> 1 & k divides a & k divides b )