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, eq_self_iff_true, xor_true] 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)
simpa only [xor_true, xor_comm] using (succ_ne_self _)