refine Int.ModEq.cancel_left_div_gcd (Nat.cast_pos.2 hp.pos) ?_
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ a (p - 2) ≡ 0 [ZMOD ↑p / ↑((↑p).gcd 6)]
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ 6 * a (p - 2) ≡ 6 * 0 [ZMOD ↑p]