for a, b being non trivial Nat st a,b are_coprime holds
( not a divides b & not b divides a )