case zero
m : ℕ
⊢ bodd (m + zero) = bxor (bodd m) (bodd zero)

case succ
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ bodd (m + succ n) = bxor (bodd m) (bodd (succ n))
m n : ℕ
⊢ bodd (m + n) = bxor (bodd m) (bodd n)
induction' n with n IH
no goals
case zero
m : ℕ
⊢ bodd (m + zero) = bxor (bodd m) (bodd zero)
simp
case succ
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ (!bxor (bodd m) (bodd n)) = bxor (bodd m) !bodd n
case succ
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ bodd (m + succ n) = bxor (bodd m) (bodd (succ n))
simp [add_succ, IH]
no goals
case succ
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ (!bxor (bodd m) (bodd n)) = bxor (bodd m) !bodd n
cases bodd m <;> cases bodd n <;> rfl