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