let a be Integer; :: thesis: ( a divides 0 & 1 divides a & - 1 divides a )
0 = a * 0 ;
hence a divides 0 ; :: thesis: ( 1 divides a & - 1 divides a )
a = 1 * a ;
hence 1 divides a ; :: thesis: - 1 divides a
a = (- 1) * (- a) ;
hence - 1 divides a ; :: thesis: verum