theorem :: INT_2:3

for a being Integer holds
( 0 divides a iff a = 0 ) ;