rw [if_pos h]
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
even : Nat.succ x % 2 = 0
h : 0 < Nat.succ x ∧ Nat.succ x % 2 = 0
⊢ (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
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
even : Nat.succ x % 2 = 0
h : 0 < Nat.succ x ∧ Nat.succ x % 2 = 0
⊢ (let vbn_half := val_bin_nat (Nat.succ x / 2);
      (vbn_half.fst + 1, vbn_half.snd)).snd ≤
    Nat.succ x