have not_even : Nat.succ (Nat.succ x) % 2 ≠ 0 := by
  rw [odd]
  simp;
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
odd : Nat.succ (Nat.succ x) % 2 = 1
⊢ 0 <
    (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
        (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ (Nat.succ x) then (0, Nat.succ (Nat.succ x)) else (0, 0)).snd
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
odd : Nat.succ (Nat.succ x) % 2 = 1
not_even : Nat.succ (Nat.succ x) % 2 ≠ 0
⊢ 0 <
    (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
        (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ (Nat.succ x) then (0, Nat.succ (Nat.succ x)) else (0, 0)).snd