intro y y_le_sx
case succ
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
⊢ ∀ (y : ℕ), y ≤ Nat.succ x → (val_bin_nat y).snd ≤ Nat.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