let k, l be Integer; :: thesis: ( k <> 0 implies ( k divides l iff l / k is Integer ) )
assume A1: k <> 0 ; :: thesis: ( k divides l iff l / k is Integer )

A2: now

assume k divides l ; :: thesis: l / k is Integer
then consider m being Integer such that
A3: l = k * m by INT_1:def 9;
thus l / k is Integer by A1, A3, XCMPLX_1:90; :: thesis: verum

end;

now

assume l / k is Integer ; :: thesis: k divides l
then reconsider m = l / k as Integer ;
l = k * m by A1, XCMPLX_1:88;
hence k divides l by INT_1:def 9; :: thesis: verum

end;

hence ( k divides l iff l / k is Integer ) by A2; :: thesis: verum