Commit 2024-09-09 14:40 f9e5fd45
View on Github →chore(Order/SuccPred/Limit): improve induction principles (#16575) This PR does the following:
- We define
isSuccPrelimitRecOn
without using tactics, which allows us to golf a proof slightly. - We define
prelimitRecOn
usingcast
instead ofEq.subst
, which is more idiomatic. - We introduce variants of
prelimitRecOn_succ
for orders without maximum elements. - Better variable management throughout.