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
- a divides a by Lm1;
hence - a divides b by A1, Lm2; :: thesis: verum
end;
assume A2: - a divides b ; :: thesis: a divides b
a divides - a by Lm1;
hence a divides b by A2, Lm2; :: thesis: verum