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
.