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