rw [odd]
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
odd : Nat.succ (Nat.succ x) % 2 = 1
⊢ Nat.succ (Nat.succ x) % 2 ≠ 0
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
odd : Nat.succ (Nat.succ x) % 2 = 1
⊢ 1 ≠ 0