let m, n, k be Element of NAT ; :: thesis: ( ( m divides n or k = 0 ) iff k * m divides k * n )

hereby :: thesis: ( not k * m divides k * n or m divides n or k = 0 )

assume A1: ( m divides n or k = 0 ) ; :: thesis: k * m divides k * n

per cases ( m divides n or k = 0 ) by A1;

suppose m divides n ; :: thesis: k * m divides k * n

then consider k9 being Nat such that
A2: n = m * k9 by NAT_D:def 3;
k * n = (k * m) * k9 by A2;
hence k * m divides k * n by NAT_D:def 3; :: thesis: verum

end;

suppose k = 0 ; :: thesis: k * m divides k * n

hence k * m divides k * n ; :: thesis: verum

end;

end;

end;

assume A3: k * m divides k * n ; :: thesis: ( m divides n or k = 0 )

now

consider k9 being Nat such that
A4: k * n = (k * m) * k9 by A3, NAT_D:def 3;
assume A5: k <> 0 ; :: thesis: m divides n
k * n = k * (m * k9) by A4;
then n = m * k9 by A5, XCMPLX_1:5;
hence m divides n by NAT_D:def 3; :: thesis: verum

end;

hence ( m divides n or k = 0 ) ; :: thesis: verum