theorem NAT31: :: NEWTON03:5

for a, b, c, d being Integer st a divides b & c divides d holds
a * c divides b * d by NAT_3:1;