rw [habs, ← ZMod.intCast_eq_intCast_iff, Int.cast_sub, ← sub_eq_zero] at hcong
p : ℕ
hpri✝ : p.Prime
k₁ k₂ : Fin p
hpri : p.Prime
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
this : Fact p.Prime
habs : ↑k₁ = ↑k₂
⊢ False
p : ℕ
hpri✝ : p.Prime
k₁ k₂ : Fin p
hpri : p.Prime
this : Fact p.Prime
hcong : ↑↑↑k₂ - (↑↑↑k₂ - ↑1) = 0
habs : ↑k₁ = ↑k₂
⊢ False