case zero
m : ℕ
⊢ bodd (m * zero) = (bodd m && bodd zero)

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