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.

Estimated changes