for a, b being Element of Gauss_INT_Ring
for aa, bb being G_INTEG st a = aa & b = bb & a divides b holds
aa Divides bb