Skip to content
Snippets Groups Projects
user avatar
Robbert Krebbers authored
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.
7ebc1859
History
Name Last commit Last update
..