cases y_le_sx with
| refl =>
  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)
| step y_le_x => exact ih y y_le_x;
case succ
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
y : ℕ
y_le_sx : y ≤ Nat.succ x
⊢ 0 < (val_bin_nat (Nat.succ y)).snd
no goals