Commit 2024-05-17 06:05 a8722d62
View on Github →chore(EllipticDivisibilitySequence): backport change for nightly-testing (#12969)
Because well-founded definitions will by default become irreducible in v4.9.0, we need to adjust some proofs here.
An alternative, which allows leaving the lemmas as by rfl (and hence eligible for dsimp) is to add @[semireducible] to preNormEDS'. However I think this is a better default.