case zero
p : ℕ
w : 0 < p
⊢ 0 ≤ 4 % (2 ^ p - 1)

case succ
p : ℕ
w : 0 < p
n✝ : ℕ
⊢ 0 ≤ (sMod p n✝ ^ 2 - 2) % (2 ^ p - 1)
p : ℕ
w : 0 < p
i : ℕ
⊢ 0 ≤ sMod p i
cases i <;> dsimp [sMod]
no goals
case zero
p : ℕ
w : 0 < p
⊢ 0 ≤ 4 % (2 ^ p - 1)
exact sup_eq_right.mp rfl
case succ.a
p : ℕ
w : 0 < p
n✝ : ℕ
⊢ 2 ^ p - 1 ≠ 0
case succ
p : ℕ
w : 0 < p
n✝ : ℕ
⊢ 0 ≤ (sMod p n✝ ^ 2 - 2) % (2 ^ p - 1)
apply Int.emod_nonneg
no goals
case succ.a
p : ℕ
w : 0 < p
n✝ : ℕ
⊢ 2 ^ p - 1 ≠ 0
exact mersenne_int_ne_zero p w