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.