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