induction n with
| one => exact Nat.one_ne_zero
| bit0 n ih =>
  rw [←Nat.mul_zero 2, asBin.toNat_bit0]
  intro h
  absurd ih
  exact Nat.eq_of_mul_eq_mul_left (Nat.is_pos 2) h
| bit1 n _ => exact Nat.succ_ne_zero (2 * n.toNat)
n : Pos.asBin
⊢ n.toNat ≠ 0
no goals