[Merged by Bors] - chore: tidy up a factorization proof

[ericrbg]

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.

---

[eric-wieser]

bors d+

Thanks! I think this was probably a result of my recent refactor of Multiset.toFinsupp.

[bors]

✌️ ericrbg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

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.

This is pretty unavoidable; the important thing is to use convert so that there's only one Eq.mpr and not a whole pile of them.

[jcommelin]

Thanks 🎉

bors merge

[ericrbg]

I completely missed that Eric had given it a d+ instead of just approving, haha

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style