let a, b be Integer; :: thesis: ( a divides b iff a divides - b )
thus ( a divides b implies a divides - b ) :: thesis: ( a divides - b implies a divides b )
proof
assume A1: a divides b ; :: thesis: a divides - b
b divides - b by Lm1;
hence a divides - b by A1, Lm2; :: thesis: verum
end;
assume A2: a divides - b ; :: thesis: a divides b
- b divides b by Lm1;
hence a divides b by A2, Lm2; :: thesis: verum