for q being G_INTEG st Norm q is Prime holds
q is g_prime