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