p i : ℕ
⊢ sMod p (i + 1) = (sMod p i * sMod p i - 2) % (2 ^ p - 1)
p : ℕ
a : ℤ
i : ℕ
b c : ℤ
h1 : 2 ^ p - 1 = a
h2 : sMod p i = b
h3 : (b * b - 2) % a = c
⊢ sMod p (i + 1) = c
substs a b c
p i : ℕ
⊢ sMod p (i + 1) = (sMod p i ^ 2 - 2) % (2 ^ p - 1)
p i : ℕ
⊢ sMod p (i + 1) = (sMod p i * sMod p i - 2) % (2 ^ p - 1)
rw [← sq]
no goals
p i : ℕ
⊢ sMod p (i + 1) = (sMod p i ^ 2 - 2) % (2 ^ p - 1)
rfl