Commit 2022-06-04 17:34 8a6a7933
View on Github →refactor(data/fin/basic): reformulate fin.strict_mono_iff_lt_succ (#14482)
Use fin.succ_cast and fin.succ. This way we lose the case n = 0
but the statement looks more natural in other cases. Also add versions
for monotone, antitone, and strict_anti.