### Revert "prelude: add notation for > and >= for all kinds of numbers"

This reverts commit 24fa20e5f8a2042caa19f1f6505102c5434cce54. Although these symmetric variants sometimes look "better", they are really annoying and should IMHO never be used: 1.) For lemmas there is now a choice between >= and <=. Since there is no longer a canonical choice, it is very easy to introduce a lot of inconsistencies in statements of lemmas. 2.) For automation the situation becomes annoying, you have to built in stuff for both >= and <=. That is very error-prone. 3.) For N and Z the notions x <= y and y >= x are not even convertible! That means that done/by does not solve x <= y if you have y >= x and if avoids you applying certain lemmas.

Showing

Please register or sign in to comment