let a, b be Integer; :: thesis: ( a divides b iff - a divides b )
A1: ( - a divides b implies a divides b )

proof

assume A2: - a divides b ; :: thesis: a divides b
a divides - a by Lm1;
hence a divides b by A2, Lm2; :: thesis: verum

end;

( a divides b implies - a divides b )

proof

assume A3: a divides b ; :: thesis: - a divides b
- a divides a by Lm1;
hence - a divides b by A3, Lm2; :: thesis: verum

end;

hence ( a divides b iff - a divides b ) by A1; :: thesis: verum