for m, n being Element of NAT st m * n is square & m,n are_coprime holds
( m is square & n is square )