let a, n be Nat; :: thesis: 5 divides (a |^ ((4 * n) + 1)) - a
4 + 1 divides (a |^ ((4 * n) + 1)) - a by PEPIN:59, Th73;
hence 5 divides (a |^ ((4 * n) + 1)) - a ; :: thesis: verum