refine (Int.even_pow' two_ne_zero).mp ?_
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
⊢ Even q
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
⊢ Even (q ^ 2)