letI : Fact (Nat.Prime p') := hpri
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
⊢ Prime (⋯.toInteger - 1)
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact (↑p').Prime := hpri
⊢ Prime (⋯.toInteger - 1)