case inl.intro
m n k : ℤ
⊢ Xor' (k + k = 2 * k) (k + k = 2 * k + 1)

case inr.intro
m n k : ℤ
⊢ Xor' (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)
m n✝ n : ℤ
⊢ ∃ k, Xor' (n = 2 * k) (n = 2 * k + 1)
rcases even_or_odd n with (⟨k, rfl⟩ | ⟨k, rfl⟩) <;> use k
no goals
case inl.intro
m n k : ℤ
⊢ Xor' (k + k = 2 * k) (k + k = 2 * k + 1)
simpa only [← two_mul, Xor', true_and_iff, eq_self_iff_true, not_true, or_false_iff,
  and_false_iff] using (succ_ne_self (2 * k)).symm
no goals
case inr.intro
m n k : ℤ
⊢ Xor' (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)
simp only [Xor', add_right_eq_self, false_or_iff, eq_self_iff_true, not_true, not_false_iff,
  one_ne_zero, and_self_iff]