no goals
h : 0 ≠ 0
⊢ 1 < bit1 0
contradiction
n : ℕ
x✝ : succ n ≠ 0
⊢ 1 < succ (succ (bit1 n))
n : ℕ
x✝ : succ n ≠ 0
⊢ 1 < bit1 (succ n)
rw [Nat.bit1_succ_eq]
case a
n : ℕ
x✝ : succ n ≠ 0
⊢ 0 < bit1 n + 1
n : ℕ
x✝ : succ n ≠ 0
⊢ 1 < succ (succ (bit1 n))
apply succ_lt_succ
no goals
case a
n : ℕ
x✝ : succ n ≠ 0
⊢ 0 < bit1 n + 1
apply zero_lt_succ