ring
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ 6 * (2 ^ (p - 2) + 3 ^ (p - 2) + 6 ^ (p - 2) - 1) =
    3 * (2 * 2 ^ (p - 2)) + 2 * (3 * 3 ^ (p - 2)) + 2 * 3 * (2 * 3) ^ (p - 2) - 6
no goals