:: deftheorem defines are_coprime PYTHTRIP:def 2 :
for m, n being Nat holds
( m,n are_coprime iff for p being prime Nat holds
( not p divides m or not p divides n ) );