chore(data/finset/basic): lemmas about `(range n).nonempty` (#8905)
chore(data/finset/basic): lemmas about `(range n).nonempty` (#8905)

Add `finset.nonempty_range_iff`, `finset.range_eq_empty_iff`, and
`range.nonempty_range_succ`.





leanprover-community/mathlib,leanprover-community/mathlib