(2 |^ 4) |^ 161,1 |^ 161 are_congruent_mod 5 by Lm1141, GR_CY_3:34;
then (2 |^ 644) * (2 |^ 1),1 * 2 are_congruent_mod 5 by Lm1124, INT_4:11;
hence 5 divides (2 |^ 645) - 2 by Lm1126; :: thesis: verum