have acc : ∀ y, (y ≤ x → 0 < (val_bin_nat (Nat.succ y)).2) := by
  induction x with
  | zero =>
    intro y y_le_x
    rw [le_zero_eq] at y_le_x
    rw [y_le_x]
    exact Nat.lt_succ_self 0 | succ x ih =>
    intro y y_le_sx
    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;
x : ℕ
⊢ 0 < (val_bin_nat (Nat.succ x)).snd
x : ℕ
acc : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
⊢ 0 < (val_bin_nat (Nat.succ x)).snd