case zero
n : ℕ
h : 0 < bit0 zero
⊢ 0 < zero

case succ
n n✝ : ℕ
h : 0 < bit0 (succ n✝)
⊢ 0 < succ n✝
n✝ n : ℕ
h : 0 < bit0 n
⊢ 0 < n
cases n
no goals
case zero
n : ℕ
h : 0 < bit0 zero
⊢ 0 < zero
cases h
no goals
case succ
n n✝ : ℕ
h : 0 < bit0 (succ n✝)
⊢ 0 < succ n✝
apply succ_pos