let a, n be Nat; :: thesis: 3 divides (a |^ ((2 * n) + 1)) - a
2 + 1 divides (a |^ ((2 * n) + 1)) - a by PEPIN:41, Th73;
hence 3 divides (a |^ ((2 * n) + 1)) - a ; :: thesis: verum