rewrite [Nat.add_assoc (n-j.1 + (m-i.1-1)), ← Nat.mul_two, Nat.mul_mod_left]
m n : Nat
i : Fin m
j : Fin n
⊢ ¬(n - ↑j + (m - ↑i - 1) + (n - ↑j) + (m - ↑i - 1)) % 2 = 1
m n : Nat
i : Fin m
j : Fin n
⊢ ¬0 = 1