From eb5638337cac97307b7c625d819e83c6fc8d80ae Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Thu, 11 Feb 2016 20:10:27 +0100
Subject: [PATCH] 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 errorprone.
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.

prelude/numbers.v  21 
1 file changed, 21 deletions()
diff git a/prelude/numbers.v b/prelude/numbers.v
index 023f91f4..65b9621e 100644
 a/prelude/numbers.v
+++ b/prelude/numbers.v
@@ 28,10 +28,6 @@ Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%nat : nat_
Notation "(≤)" := le (only parsing) : nat_scope.
Notation "(<)" := lt (only parsing) : nat_scope.
Infix "≥" := ge : nat_scope.
Notation "(≥)" := ge (only parsing) : nat_scope.
Notation "(>)" := gt (only parsing) : nat_scope.

Infix "`div`" := Nat.div (at level 35) : nat_scope.
Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
@@ 108,10 +104,6 @@ Notation "(<)" := Pos.lt (only parsing) : positive_scope.
Notation "(~0)" := xO (only parsing) : positive_scope.
Notation "(~1)" := xI (only parsing) : positive_scope.
Infix "≥" := Pos.ge : positive_scope.
Notation "(≥)" := Pos.ge (only parsing) : positive_scope.
Notation "(>)" := Pos.gt (only parsing) : positive_scope.

Arguments Pos.of_nat _ : simpl never.
Instance positive_eq_dec: ∀ x y : positive, Decision (x = y) := Pos.eq_dec.
Instance positive_inhabited: Inhabited positive := populate 1.
@@ 187,11 +179,6 @@ Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%N : N_scope.
Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%N : N_scope.
Notation "(≤)" := N.le (only parsing) : N_scope.
Notation "(<)" := N.lt (only parsing) : N_scope.

Infix "≥" := N.ge : N_scope.
Notation "(≥)" := N.ge (only parsing) : N_scope.
Notation "(>)" := N.gt (only parsing) : N_scope.

Infix "`div`" := N.div (at level 35) : N_scope.
Infix "`mod`" := N.modulo (at level 35) : N_scope.
@@ 226,10 +213,6 @@ Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Z_scope.
Notation "(≤)" := Z.le (only parsing) : Z_scope.
Notation "(<)" := Z.lt (only parsing) : Z_scope.
Infix "≥" := Z.ge : Z_scope.
Notation "(≥)" := Z.ge (only parsing) : Z_scope.
Notation "(>)" := Z.gt (only parsing) : Z_scope.

Infix "`div`" := Z.div (at level 35) : Z_scope.
Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
Infix "`quot`" := Z.quot (at level 35) : Z_scope.
@@ 345,10 +328,6 @@ Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Qc_scope
Notation "(≤)" := Qcle (only parsing) : Qc_scope.
Notation "(<)" := Qclt (only parsing) : Qc_scope.
Infix "≥" := Qcge : Qc_scope.
Notation "(≥)" := Qcge (only parsing) : Qc_scope.
Notation "(>)" := Qcgt (only parsing) : Qc_scope.

Hint Extern 1 (_ ≤ _) => reflexivity  discriminate.
Arguments Qred _ : simpl never.

2.26.2