have hp' : p - 1 = p - 2 + 1 := Eq.symm <| Nat.succ_pred <| (tsub_pos_of_lt hp.one_lt).ne'
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
⊢ ↑p ∣ a (p - 2)
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ ↑p ∣ a (p - 2)