n✝ n : ℕ
⊢ boddDiv2 n = ((boddDiv2 n).fst, (boddDiv2 n).snd)
n✝ n : ℕ
⊢ boddDiv2 n = (bodd n, div2 n)
unfold bodd div2
case mk
n✝ n : ℕ
fst✝ : Bool
snd✝ : ℕ
⊢ (fst✝, snd✝) = ((fst✝, snd✝).fst, (fst✝, snd✝).snd)
n✝ n : ℕ
⊢ boddDiv2 n = ((boddDiv2 n).fst, (boddDiv2 n).snd)
cases boddDiv2 n
no goals
case mk
n✝ n : ℕ
fst✝ : Bool
snd✝ : ℕ
⊢ (fst✝, snd✝) = ((fst✝, snd✝).fst, (fst✝, snd✝).snd)
rfl