consider f being Function of the carrier of Gauss_INT_Ring,NAT such that
A1: for x being G_INTEG holds f . x = Norm x by Lm13;
for a, b being Element of Gauss_INT_Ring st b <> 0. Gauss_INT_Ring holds
ex q, r being Element of Gauss_INT_Ring st
( a = (q * b) + r & ( r = 0. Gauss_INT_Ring or f . r < f . b ) ) by Lm14, A1;
hence Gauss_INT_Ring is Euclidian by INT_3:def 8; :: thesis: verum