α : Type u_1
inst✝ : LinearOrderedSemiring α
n : PosNum
⊢ 1 ≤ ↑n
α : Type u_1
inst✝ : LinearOrderedSemiring α
n : PosNum
⊢ 1 ≤ ↑n
rw [← cast_to_nat, ← Nat.cast_one, Nat.cast_le (α := α)]
no goals
α : Type u_1
inst✝ : LinearOrderedSemiring α
n : PosNum
⊢ 1 ≤ ↑n
apply to_nat_pos