From 91e2e89e84c0eb343198b0c887b727b35f9658cd Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 29 Apr 2006 11:55:57 +0000
Subject: qq proprietes de plus sur Ncompare

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8771 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/NArith/BinNat.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index fef8ac8389..f79d09b51d 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -247,6 +247,18 @@ destruct n as [| n]; destruct m as [| m]; simpl in |- *; intro H;
   rewrite (Pcompare_Eq_eq n m H); reflexivity.
 Qed.
 
+Lemma Ncompare_refl : forall n, (n ?= n) = Eq.
+Proof.
+destruct n; simpl; auto.
+apply Pcompare_refl.
+Qed.
+
+Lemma Ncompare_antisym : forall n m, CompOpp (n ?= m) = (m ?= n).
+Proof.
+destruct n; destruct m; simpl; auto.
+exact (Pcompare_antisym p p0 Eq).
+Qed.
+
 (** Dividing by 2 *)
 
 Definition Ndiv2 (n:N) :=
-- 
cgit v1.2.3