cases y_le_sx with
| refl =>
  cases mod_two_eq_zero_or_one (Nat.succ x) with
  | inl even =>
    have h : 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 :=
    And.intro (zero_lt_succ x) even;
    show (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
    let vbn_half := val_bin_nat (Nat.succ x / 2);
    (vbn_half.fst + 1, vbn_half.snd)
    else if 0 < Nat.succ x then
    (0, Nat.succ x)
    else
    (0, 0)).snd ≤ Nat.succ x
    rw [if_pos h]
    have h' := ih (Nat.succ x / 2) (div2_succ_le_self x);
    exact le_trans h' (le_succ x)
  | inr odd =>
    show (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
    let vbn_half := val_bin_nat (Nat.succ x / 2);
    (vbn_half.fst + 1, vbn_half.snd)
    else if 0 < Nat.succ x then
    (0, Nat.succ x)
    else
    (0, 0)).snd ≤ Nat.succ x
    have not_even : Nat.succ x % 2 ≠ 0 := by
      rw [odd]
      simp;
    rw [if_neg (not_and_of_not_right (0 < Nat.succ x) not_even)]
    rw [if_pos (zero_lt_succ x)]
| step y_le_x => exact le_trans (ih y y_le_x) (le_succ x);
case succ
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
y : ℕ
y_le_sx : y ≤ Nat.succ x
⊢ (val_bin_nat y).snd ≤ Nat.succ x
no goals