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