have : (2^p - 1) % q = 0 :=  mod_eq_zero_of_dvd (minFac_dvd m)
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
⊢ q.ModEq (2 ^ p) 1
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
this : (2 ^ p - 1) % q = 0
⊢ q.ModEq (2 ^ p) 1