cases mod_two_eq_zero_or_one (Nat.succ (Nat.succ x)) with
| inl even =>
  have h : 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 :=
  And.intro (zero_lt_succ (Nat.succ x)) even;
  show 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
  rw [if_pos h, div2_succ_succ_eq_succ_div2]
  exact ih (x / 2) (Nat.div_le_self x 2)
| inr odd =>
  show 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
  have not_even : Nat.succ (Nat.succ x) % 2 ≠ 0 := by
    rw [odd]
    simp;
  rw [if_neg (not_and_of_not_right (0 < Nat.succ (Nat.succ x)) not_even)]
  rw [if_pos (zero_lt_succ (Nat.succ x))]
  exact zero_lt_succ (Nat.succ x)
case succ.refl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
⊢ 0 < (val_bin_nat (Nat.succ (Nat.succ x))).snd
no goals