let a, n be Nat; :: thesis: ( a > 1 implies a - 1 divides (a |^ n) - 1 )
assume A1: a > 1 ; :: thesis: a - 1 divides (a |^ n) - 1
A2: (2 |^ n) - 1 is Nat by PREPOWER:19, NAT_1:21;
A3: a >= 1 + 1 by NAT_1:13, A1;

per cases ( a = 2 or a > 2 ) by A3, XXREAL_0:1;

suppose A4: a = 2 ; :: thesis: a - 1 divides (a |^ n) - 1

then ((a |^ n) - 1) mod (a - 1) = 0 by RADIX_2:1, A2;
hence a - 1 divides (a |^ n) - 1 by INT_1:89, A4; :: thesis: verum

end;

suppose A5: a > 2 ; :: thesis: a - 1 divides (a |^ n) - 1

then A6: a - 1 > 2 - 1 by XREAL_1:11;
A7: a - 1 is Nat by NAT_1:20, A5;
a mod (a - 1) = (a + ((a - 1) * (- 1))) mod (a - 1) by INT_3:8
.= 1 by PEPIN:5, A6 ;
then A8: (a |^ n) mod (a - 1) = 1 by PEPIN:36, A6, A7;
((a |^ n) - 1) mod (a - 1) = (((a |^ n) mod (a - 1)) - (1 mod (a - 1))) mod (a - 1) by INT_6:7
.= (1 - 1) mod (a - 1) by PEPIN:5, A6, A8
.= 0 by NAT_D:26, A7 ;
hence a - 1 divides (a |^ n) - 1 by INT_1:89, A6, A7; :: thesis: verum

end;

end;