simp [cast_one, cast_pow, cast_ofNat, hc.symm]
case h
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
c : ℤ
hc : -↑(2 ^ p - 1) = c * ↑q
⊢ ↑1 - ↑(2 ^ p) = c * ↑q
no goals