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