255 = 17 * 15 ;
then 2 |^ 8,1 are_congruent_mod 17 by Lm8;
then (2 |^ 8) |^ 5,1 |^ 5 are_congruent_mod 17 by GR_CY_3:34;
then (2 |^ 40) * 2,1 * 2 are_congruent_mod 17 by Lm1125, INT_4:11;
then A1: 2 |^ (40 + 1),2 are_congruent_mod 17 by NEWTON:6;
2 |^ 56,1 |^ 7 are_congruent_mod 17 by Lm1144, Lm1145, Lm1146, INT_1:15;
then (2 |^ 56) |^ 19,1 |^ 19 are_congruent_mod 17 by GR_CY_3:34;
then (2 |^ 1064) * (2 |^ 41),1 * (2 |^ 41) are_congruent_mod 17 by Lm1130, INT_4:11;
then 2 |^ 1105,2 are_congruent_mod 17 by A1, Lm1131, INT_1:15;
hence 17 divides (2 |^ 1105) - 2 ; :: thesis: verum