rw [if_pos (zero_lt_succ x)]
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
odd : Nat.succ x % 2 = 1
not_even : Nat.succ x % 2 ≠ 0
⊢ (if 0 < Nat.succ x then (0, Nat.succ x) else (0, 0)).snd ≤ Nat.succ x
no goals