environ
vocabularies HIDDEN, NUMBERS, INT_1, ORDINAL1, COMPLEX1, SUBSET_1, XXREAL_0, CARD_1, ARYTM_3, ARYTM_1, RELAT_1, NAT_1, XCMPLX_0, INT_2;
notations HIDDEN, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_1, NAT_1, COMPLEX1, XXREAL_0;
definitions INT_1;
theorems INT_1, ABSVALUE, NAT_1, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1;
schemes NAT_1;
registrations XREAL_0, NAT_1, INT_1, ORDINAL1, CARD_1;
constructors HIDDEN, XXREAL_0, REAL_1, NAT_1, COMPLEX1, INT_1, CARD_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, ARITHM, BOOLE;
equalities ;
expansions INT_1;
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 i, j being Nat st 0 < j & i divides j holds
i <= j