OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12250 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 15 insertions, 0 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 84af2fe85..147d1e8d3 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -206,6 +206,21 @@ Definition CompOpp (r:comparison) :=
     | Gt => Lt
   end.
 
+Lemma CompOpp_involutive : forall c, CompOpp (CompOpp c) = c.
+Proof.
+  destruct c; reflexivity.
+Qed.
+
+Lemma CompOpp_inj : forall c c', CompOpp c = CompOpp c' -> c = c'.
+Proof.
+  destruct c; destruct c'; auto; discriminate.
+Qed.
+
+Lemma CompOpp_iff : forall c c', CompOpp c = c' <-> c = CompOpp c'.
+Proof.
+  split; intros; apply CompOpp_inj; rewrite CompOpp_involutive; auto.
+Qed.
+
 (** Identity *)
 
 Definition ID := forall A:Type, A -> A.