simp only [CharP.cast_eq_zero, ge_iff_le, gt_iff_lt, pow_pos, cast_pred, cast_pow, cast_ofNat,
    zero_sub, neg_sub] at hc
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 : ↑0 - ↑(2 ^ p - 1) = c * ↑q
⊢ ↑1 - ↑(2 ^ p) = c * ↑q
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