a gcd b divides a by INT_2:def 2;
then consider k being Integer such that
A1: a = (a gcd b) * k ;
thus a / (a gcd b) is integer by A1, XCMPLX_1:89; :: thesis: verum