Commit 2023-09-18 15:32 6aa66faf
View on Github →chore: tidy up a factorization proof (#7164)
This used to not work because the finsupp poisoned the computability, but it seems fine now. Also slightly tidied it whilst I was there.
However, I'm not sure if this is actually wise to keep as something towards Sort*: the created term on k + 2 is not pretty and has an Eq.mpr.