for p, q being Nat st p is prime & q is prime & not p,q are_coprime holds
p = q