add Compare operational typeclass

[palmskog]

Here is an initial draft adding the Compare operational typeclass discussed in #74.

There are some low-level improvements to make, but also some questions to think about:

• Should there be any infix notation at all for the Compare typeclass? I add here x <?> y, but I don't use it in the code, since it's such as big change.
• I get rid of some more boolean functions for convenience. I think it looks reasonable, but there are some tradeoffs in that the Decision typeclass shows up in a lot of places.

@Casteran could you give a high-level assessment whether this PR is worth polishing up and merging? Or maybe it should stay an experiment?

[Casteran]

Here is an initial draft adding the Compare operational typeclass discussed in #74.

Thanks !

There are some low-level improvements to make, but also some questions to think about:

* Should there be any infix notation at all for the Compare typeclass? I add here `x <?> y`, but I don't use it in the code, since it's such as big change.

May be we can just give the infix for a kind of compatibility with the notations in Standard Library. Personally, I will use
the synstx "compare x y" in the code.

* I get rid of some more boolean functions for convenience. I think it looks reasonable, but there are some tradeoffs in that the Decision typeclass shows up in a lot of places.

@Casteran could you give a high-level assessment whether this PR is worth polishing up and merging? Or maybe it should stay an experiment?

I have had a look at your code, and found very reasonable to get rid of the boolean function whenever possible.
We do not have sequences like unfold lt, lt_bany more :-)

The cost will be perhaps to add a documentation on Decision in the book (but it will be interesting anyway !).

[palmskog]

I improved the organization of lemmas and did some fixes based on the discussion above. In particular, I removed the infix notation for compare for now and updated some material on the Comparable typeclass for the new (in my opinion improved) definition. I think this should now be ready to merge.

Since the Decision typeclass was not the subject of this PR, I would prefer to another PR with material in the book about Decision.