Theorem: Pos.one_le (Extra/Pos/Lemmas.lean)

State before:
x : Pos
⊢ 1 ≤ x
Tactic:
by_toNat
State after:
x : Pos
⊢ x.toNat ≥ 1

State before:
x : Pos
⊢ x.toNat ≥ 1
Tactic:
apply Nat.succ_le_of_lt
State after:
case h
x : Pos
⊢ 0 < x.toNat

State before:
case h
x : Pos
⊢ 0 < x.toNat
Tactic:
exact Nat.zero_lt _
State after:
no goals