x : WithBot ℕ
h : 0 < x
⊢ 1 ≤ x
x : WithBot ℕ
⊢ 1 ≤ x ↔ 0 < x
refine' ⟨fun h => lt_of_lt_of_le (WithBot.coe_lt_coe.mpr zero_lt_one) h, fun h => _⟩
case bot
h : 0 < ⊥
⊢ 1 ≤ ⊥

case coe
a✝ : ℕ
h : 0 < ↑a✝
⊢ 1 ≤ ↑a✝
x : WithBot ℕ
h : 0 < x
⊢ 1 ≤ x
induction x using WithBot.recBotCoe
no goals
case bot
h : 0 < ⊥
⊢ 1 ≤ ⊥
exact (not_lt_bot h).elim
no goals
case coe
a✝ : ℕ
h : 0 < ↑a✝
⊢ 1 ≤ ↑a✝
exact WithBot.coe_le_coe.mpr (Nat.succ_le_iff.mpr (WithBot.coe_lt_coe.mp h))