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 :: thesis: ( l / k is Integer implies k divides l )

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

end;

now :: thesis: ( k divides l implies l / k is Integer )

assume k divides l ; :: thesis: l / k is Integer
then ex m being Integer st l = k * m by INT_1:def 3;
hence l / k is Integer by A1, XCMPLX_1:89; :: thesis: verum

end;

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