have h : 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 :=
And.intro (zero_lt_succ x) even
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
even : Nat.succ x % 2 = 0
⊢ (val_bin_nat (Nat.succ x)).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
⊢ (val_bin_nat (Nat.succ x)).snd ≤ Nat.succ x