begin
Lm1:
for a being Integer holds
( a divides - a & - a divides a )
Lm2:
for a, b, c being Integer st a divides b & b divides c holds
a divides c
Lm3:
for a, b being Integer holds
( a divides b iff a divides - b )
Lm4:
for a, b being Integer holds
( a divides b iff - a divides b )
Lm5:
for a being Integer holds
( a divides 0 & 1 divides a & - 1 divides a )
Lm6:
for a, b, c being Integer st a divides b & a divides c holds
a divides b mod c
Lm7:
for k, l being Nat holds
( k divides l iff ex t being Nat st l = k * t )
Lm8:
for i, j being Nat st i divides j & j divides i holds
i = j
Lm9:
for j, i being Nat st 0 < j & i divides j holds
i <= j
begin