haveI : Fact p.Prime := ⟨hpri⟩
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑(-1)
this : NeZero p
⊢ (-1).val = p - 1
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑(-1)
this✝ : NeZero p
this : Fact p.Prime
⊢ (-1).val = p - 1