Faunwell. It was magnificent while it lasted... https://www.youtube.com/watch?v=OFIVy79pgWc

Playing MiSide at midnight wasn't a good idea.

??? time

Now it is just a small matter of updating the docs, other minor occurrences of cmp and making the PR.

Done rewriting RBSet, RBMap, their theorems and operations to use Ord. 5 files changed, 319 insertions(+), 298 deletions(-) It is now usable as it is. I now have to get rid of cmp in WF (Well-formedness) too.

Done rewriting RBSet, RBMap, their theorems and operations to use Ord. 5 files changed, 319 insertions(+), 298 deletions(-) It is now usable as it is. I now have to get rid of cmp in WF (Well-formedness) too.

Done rewriting RBSet, RBMap, their theorems and operations to use Ord.

5 files changed, 319 insertions(+), 298 deletions(\-)

It is now usable as it is. I now have to get rid of cmp in WF (Well-formedness) too.

Defeated the termination checker of Lean 4 for the first time in my life.