n : ℕ
⊢ (match boddDiv2 n with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (boddDiv2 n).fst then succ (boddDiv2 n).snd else (boddDiv2 n).snd
n : ℕ
⊢ div2 (succ n) = bif bodd n then succ (div2 n) else div2 n
simp only [bodd, boddDiv2, div2]
case mk
n : ℕ
fst : Bool
snd : ℕ
⊢ (match (fst, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (fst, snd).fst then succ (fst, snd).snd else (fst, snd).snd
n : ℕ
⊢ (match boddDiv2 n with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (boddDiv2 n).fst then succ (boddDiv2 n).snd else (boddDiv2 n).snd
cases' boddDiv2 n with fst snd
case mk.false
n snd : ℕ
⊢ (match (false, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (false, snd).fst then succ (false, snd).snd else (false, snd).snd

case mk.true
n snd : ℕ
⊢ (match (true, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (true, snd).fst then succ (true, snd).snd else (true, snd).snd
case mk
n : ℕ
fst : Bool
snd : ℕ
⊢ (match (fst, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (fst, snd).fst then succ (fst, snd).snd else (fst, snd).snd
cases fst
case mk.true
n snd : ℕ
⊢ (match (true, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (true, snd).fst then succ (true, snd).snd else (true, snd).snd
case mk.false
n snd : ℕ
⊢ (match (false, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (false, snd).fst then succ (false, snd).snd else (false, snd).snd

case mk.true
n snd : ℕ
⊢ (match (true, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (true, snd).fst then succ (true, snd).snd else (true, snd).snd
case mk.false =>
  simp
no goals
case mk.true
n snd : ℕ
⊢ (match (true, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (true, snd).fst then succ (true, snd).snd else (true, snd).snd
case mk.true =>
  simp
no goals
n snd : ℕ
⊢ (match (false, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (false, snd).fst then succ (false, snd).snd else (false, snd).snd
simp
no goals
n snd : ℕ
⊢ (match (true, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (true, snd).fst then succ (true, snd).snd else (true, snd).snd
simp