# Commit 2024-09-29 17:58 cea0638b

View on Github →feat: `fin_omega`

, a wrapper around `omega`

to help with `Fin`

arithmetic goals. (#16651)
This is a hack, and that results in `omega`

having to deal with a lot of case splitting, but it is usable.
The simp set could probably be expanded a bit, and I've left a comment inviting such changes.
This was inspired by #15817, and in particular replaces the new proof added in that PR with `by fin_omega`

.