a b : ℤ
n : ℕ
i : ℤ
⊢ (-i - i) % 2 = 0
a b : ℤ
n : ℕ
i : ℤ
⊢ -i % 2 = i % 2
apply Int.emod_eq_emod_iff_emod_sub_eq_zero.mpr
case h.e'_2.h.e'_5
a b : ℤ
n : ℕ
i : ℤ
⊢ -i - i = 2 * -i
a b : ℤ
n : ℕ
i : ℤ
⊢ (-i - i) % 2 = 0
convert Int.mul_emod_right 2 (-i) using 2
no goals
case h.e'_2.h.e'_5
a b : ℤ
n : ℕ
i : ℤ
⊢ -i - i = 2 * -i
rw [two_mul, sub_eq_add_neg]