begin
Lm1:
for t being Integer holds
( t < 1 iff t <= 0 )
Lm2:
for a being Nat st a <> 0 holds
a - 1 >= 0
Lm3:
for z being Integer holds 1 gcd z = 1
theorem
theorem Th2:
Lm4:
for m being Nat
for z being Integer st 1 - m <= z & z <= m - 1 & m divides z holds
z = 0
theorem
canceled;
theorem
canceled;
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem Th9:
theorem
theorem Th11:
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th25:
begin
:: deftheorem Def1 defines mod EULER_2:def 1 :
theorem
theorem Th27:
theorem
theorem
theorem
theorem
theorem
begin
theorem Th33:
theorem