Skip to content
  • Robbert Krebbers's avatar
    Revert "prelude: add notation for > and >= for all kinds of numbers" · eb563833
    Robbert Krebbers authored
    This reverts commit 24fa20e5.
    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.